MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin23lem26 Structured version   Visualization version   GIF version

Theorem fin23lem26 9260
Description: Lemma for fin23lem22 9262. (Contributed by Stefan O'Rear, 1-Nov-2014.)
Assertion
Ref Expression
fin23lem26 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖)
Distinct variable group:   𝑖,𝑗,𝑆

Proof of Theorem fin23lem26
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4764 . . . 4 (𝑖 = ∅ → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ ∅))
21rexbidv 3154 . . 3 (𝑖 = ∅ → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ ∅))
3 breq2 4764 . . . 4 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
43rexbidv 3154 . . 3 (𝑖 = 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
5 breq2 4764 . . . 4 (𝑖 = suc 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ suc 𝑎))
65rexbidv 3154 . . 3 (𝑖 = suc 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
7 ordom 7191 . . . . . 6 Ord ω
87a1i 11 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → Ord ω)
9 simpl 474 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
10 0fin 8304 . . . . . . . 8 ∅ ∈ Fin
11 eleq1 2791 . . . . . . . 8 (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
1210, 11mpbiri 248 . . . . . . 7 (𝑆 = ∅ → 𝑆 ∈ Fin)
1312necon3bi 2922 . . . . . 6 𝑆 ∈ Fin → 𝑆 ≠ ∅)
1413adantl 473 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
15 tz7.5 5857 . . . . 5 ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
168, 9, 14, 15syl3anc 1439 . . . 4 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
17 en0 8135 . . . . . 6 ((𝑗𝑆) ≈ ∅ ↔ (𝑗𝑆) = ∅)
18 incom 3913 . . . . . . 7 (𝑗𝑆) = (𝑆𝑗)
1918eqeq1i 2729 . . . . . 6 ((𝑗𝑆) = ∅ ↔ (𝑆𝑗) = ∅)
2017, 19bitri 264 . . . . 5 ((𝑗𝑆) ≈ ∅ ↔ (𝑆𝑗) = ∅)
2120rexbii 3143 . . . 4 (∃𝑗𝑆 (𝑗𝑆) ≈ ∅ ↔ ∃𝑗𝑆 (𝑆𝑗) = ∅)
2216, 21sylibr 224 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ ∅)
23 simplrl 819 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
24 omsson 7186 . . . . . . . . . . 11 ω ⊆ On
2523, 24syl6ss 3721 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
2625ssdifssd 3856 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
27 simplr 809 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ∈ Fin)
28 ssel2 3704 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → 𝑗 ∈ ω)
29 onfin2 8268 . . . . . . . . . . . . . . . . 17 ω = (On ∩ Fin)
30 inss2 3942 . . . . . . . . . . . . . . . . 17 (On ∩ Fin) ⊆ Fin
3129, 30eqsstri 3741 . . . . . . . . . . . . . . . 16 ω ⊆ Fin
32 peano2 7203 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
3331, 32sseldi 3707 . . . . . . . . . . . . . . 15 (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
3428, 33syl 17 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
3534adantlr 753 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
36 ssfi 8296 . . . . . . . . . . . . . 14 ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
3736ex 449 . . . . . . . . . . . . 13 (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3835, 37syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3927, 38mtod 189 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
40 ssdif0 4050 . . . . . . . . . . . 12 (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
4140necon3bbii 2943 . . . . . . . . . . 11 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
4239, 41sylib 208 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
4342ad2ant2lr 801 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
44 onint 7112 . . . . . . . . 9 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4526, 43, 44syl2anc 696 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4645eldifad 3692 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ 𝑆)
47 simprr 813 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑗𝑆) ≈ 𝑎)
48 vex 3307 . . . . . . . . . . 11 𝑗 ∈ V
49 vex 3307 . . . . . . . . . . 11 𝑎 ∈ V
50 en2sn 8153 . . . . . . . . . . 11 ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
5148, 49, 50mp2an 710 . . . . . . . . . 10 {𝑗} ≈ {𝑎}
5251a1i 11 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
53 simprl 811 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗𝑆)
5423, 53sseldd 3710 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
55 nnord 7190 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
5654, 55syl 17 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord 𝑗)
57 ordirr 5854 . . . . . . . . . . . 12 (Ord 𝑗 → ¬ 𝑗𝑗)
58 inss1 3941 . . . . . . . . . . . . 13 (𝑗𝑆) ⊆ 𝑗
5958sseli 3705 . . . . . . . . . . . 12 (𝑗 ∈ (𝑗𝑆) → 𝑗𝑗)
6057, 59nsyl 135 . . . . . . . . . . 11 (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗𝑆))
61 disjsn 4353 . . . . . . . . . . 11 (((𝑗𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗𝑆))
6260, 61sylibr 224 . . . . . . . . . 10 (Ord 𝑗 → ((𝑗𝑆) ∩ {𝑗}) = ∅)
6356, 62syl 17 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∩ {𝑗}) = ∅)
64 nnord 7190 . . . . . . . . . . . 12 (𝑎 ∈ ω → Ord 𝑎)
65 ordirr 5854 . . . . . . . . . . . 12 (Ord 𝑎 → ¬ 𝑎𝑎)
6664, 65syl 17 . . . . . . . . . . 11 (𝑎 ∈ ω → ¬ 𝑎𝑎)
67 disjsn 4353 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎𝑎)
6866, 67sylibr 224 . . . . . . . . . 10 (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
6968ad2antrr 764 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
70 unen 8156 . . . . . . . . 9 ((((𝑗𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
7147, 52, 63, 69, 70syl22anc 1440 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
72 simprr 813 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑏𝑆)
73 simplrl 819 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ ω)
7473, 24syl6ss 3721 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ On)
75 ordsuc 7131 . . . . . . . . . . . . . . . . . 18 (Ord 𝑗 ↔ Ord suc 𝑗)
7656, 75sylib 208 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord suc 𝑗)
7776adantrr 755 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → Ord suc 𝑗)
78 simp2 1129 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
7978ssdifssd 3856 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
80 simpl1 1204 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏𝑆)
81 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
8280, 81eldifd 3691 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
8382ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗𝑏 ∈ (𝑆 ∖ suc 𝑗)))
84 onnmin 7120 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 (𝑆 ∖ suc 𝑗))
8579, 83, 84syl6an 569 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 (𝑆 ∖ suc 𝑗)))
8685con4d 114 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
8786imp 444 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
88 simp3 1130 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
89 ordsucss 7135 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
9190imp 444 . . . . . . . . . . . . . . . . . . . 20 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
9291sscond 3855 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
93 intss 4606 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
9492, 93syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
95 simpl2 1206 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
96 ordelon 5860 . . . . . . . . . . . . . . . . . . . 20 ((Ord suc 𝑗𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
9788, 96sylan 489 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
98 onmindif 5928 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 (𝑆 ∖ suc 𝑏))
9995, 97, 98syl2anc 696 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑏))
10094, 99sseldd 3710 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑗))
10187, 100impbida 913 . . . . . . . . . . . . . . . 16 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
10272, 74, 77, 101syl3anc 1439 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
103 df-suc 5842 . . . . . . . . . . . . . . . 16 suc 𝑗 = (𝑗 ∪ {𝑗})
104103eleq2i 2795 . . . . . . . . . . . . . . 15 (𝑏 ∈ suc 𝑗𝑏 ∈ (𝑗 ∪ {𝑗}))
105102, 104syl6bb 276 . . . . . . . . . . . . . 14 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
106105expr 644 . . . . . . . . . . . . 13 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏𝑆 → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
107106pm5.32rd 675 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆)))
108 elin 3904 . . . . . . . . . . . 12 (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆))
109 elin 3904 . . . . . . . . . . . 12 (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆))
110107, 108, 1093bitr4g 303 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
111110eqrdv 2722 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
112 indir 3983 . . . . . . . . . 10 ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆))
113111, 112syl6eq 2774 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)))
114 snssi 4447 . . . . . . . . . . . 12 (𝑗𝑆 → {𝑗} ⊆ 𝑆)
115 df-ss 3694 . . . . . . . . . . . 12 ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
116114, 115sylib 208 . . . . . . . . . . 11 (𝑗𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
117116uneq2d 3875 . . . . . . . . . 10 (𝑗𝑆 → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
118117ad2antrl 766 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
119113, 118eqtrd 2758 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ {𝑗}))
120 df-suc 5842 . . . . . . . . 9 suc 𝑎 = (𝑎 ∪ {𝑎})
121120a1i 11 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
12271, 119, 1213brtr4d 4792 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
123 ineq1 3915 . . . . . . . . 9 (𝑏 = (𝑆 ∖ suc 𝑗) → (𝑏𝑆) = ( (𝑆 ∖ suc 𝑗) ∩ 𝑆))
124123breq1d 4770 . . . . . . . 8 (𝑏 = (𝑆 ∖ suc 𝑗) → ((𝑏𝑆) ≈ suc 𝑎 ↔ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
125124rspcev 3413 . . . . . . 7 (( (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
12646, 122, 125syl2anc 696 . . . . . 6 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
127126rexlimdvaa 3134 . . . . 5 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎))
128 ineq1 3915 . . . . . . 7 (𝑏 = 𝑗 → (𝑏𝑆) = (𝑗𝑆))
129128breq1d 4770 . . . . . 6 (𝑏 = 𝑗 → ((𝑏𝑆) ≈ suc 𝑎 ↔ (𝑗𝑆) ≈ suc 𝑎))
130129cbvrexv 3275 . . . . 5 (∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)
131127, 130syl6ib 241 . . . 4 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
132131ex 449 . . 3 (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)))
1332, 4, 6, 22, 132finds2 7211 . 2 (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
134133impcom 445 1 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  wne 2896  wrex 3015  Vcvv 3304  cdif 3677  cun 3678  cin 3679  wss 3680  c0 4023  {csn 4285   cint 4583   class class class wbr 4760  Ord word 5835  Oncon0 5836  suc csuc 5838  ωcom 7182  cen 8069  Fincfn 8072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-br 4761  df-opab 4821  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-om 7183  df-1o 7680  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076
This theorem is referenced by:  fin23lem23  9261
  Copyright terms: Public domain W3C validator