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

Theorem fin23lem26 10342
Description: Lemma for fin23lem22 10344. (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 5146 . . . 4 (𝑖 = ∅ → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ ∅))
21rexbidv 3173 . . 3 (𝑖 = ∅ → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ ∅))
3 breq2 5146 . . . 4 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
43rexbidv 3173 . . 3 (𝑖 = 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
5 breq2 5146 . . . 4 (𝑖 = suc 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ suc 𝑎))
65rexbidv 3173 . . 3 (𝑖 = suc 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
7 ordom 7874 . . . . 5 Ord ω
8 simpl 482 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9 0fin 9189 . . . . . . . 8 ∅ ∈ Fin
10 eleq1 2816 . . . . . . . 8 (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
119, 10mpbiri 258 . . . . . . 7 (𝑆 = ∅ → 𝑆 ∈ Fin)
1211necon3bi 2962 . . . . . 6 𝑆 ∈ Fin → 𝑆 ≠ ∅)
1312adantl 481 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14 tz7.5 6384 . . . . 5 ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
157, 8, 13, 14mp3an2i 1463 . . . 4 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
16 en0 9031 . . . . . 6 ((𝑗𝑆) ≈ ∅ ↔ (𝑗𝑆) = ∅)
17 incom 4197 . . . . . . 7 (𝑗𝑆) = (𝑆𝑗)
1817eqeq1i 2732 . . . . . 6 ((𝑗𝑆) = ∅ ↔ (𝑆𝑗) = ∅)
1916, 18bitri 275 . . . . 5 ((𝑗𝑆) ≈ ∅ ↔ (𝑆𝑗) = ∅)
2019rexbii 3089 . . . 4 (∃𝑗𝑆 (𝑗𝑆) ≈ ∅ ↔ ∃𝑗𝑆 (𝑆𝑗) = ∅)
2115, 20sylibr 233 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ ∅)
22 simplrl 776 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23 omsson 7868 . . . . . . . . . . 11 ω ⊆ On
2422, 23sstrdi 3990 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
2524ssdifssd 4138 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26 simplr 768 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ∈ Fin)
27 ssel2 3973 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → 𝑗 ∈ ω)
28 onfin2 9249 . . . . . . . . . . . . . . . . 17 ω = (On ∩ Fin)
29 inss2 4225 . . . . . . . . . . . . . . . . 17 (On ∩ Fin) ⊆ Fin
3028, 29eqsstri 4012 . . . . . . . . . . . . . . . 16 ω ⊆ Fin
31 peano2 7890 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
3230, 31sselid 3976 . . . . . . . . . . . . . . 15 (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
3327, 32syl 17 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
3433adantlr 714 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
35 ssfi 9191 . . . . . . . . . . . . . 14 ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
3635ex 412 . . . . . . . . . . . . 13 (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3734, 36syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3826, 37mtod 197 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39 ssdif0 4359 . . . . . . . . . . . 12 (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
4039necon3bbii 2983 . . . . . . . . . . 11 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
4138, 40sylib 217 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
4241ad2ant2lr 747 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43 onint 7787 . . . . . . . . 9 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4425, 42, 43syl2anc 583 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4544eldifad 3956 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46 simprr 772 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑗𝑆) ≈ 𝑎)
47 en2sn 9059 . . . . . . . . . . 11 ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
4847el2v 3477 . . . . . . . . . 10 {𝑗} ≈ {𝑎}
4948a1i 11 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50 simprl 770 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗𝑆)
5122, 50sseldd 3979 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52 nnord 7872 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
5351, 52syl 17 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord 𝑗)
54 ordirr 6381 . . . . . . . . . . . 12 (Ord 𝑗 → ¬ 𝑗𝑗)
55 elinel1 4191 . . . . . . . . . . . 12 (𝑗 ∈ (𝑗𝑆) → 𝑗𝑗)
5654, 55nsyl 140 . . . . . . . . . . 11 (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗𝑆))
57 disjsn 4711 . . . . . . . . . . 11 (((𝑗𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗𝑆))
5856, 57sylibr 233 . . . . . . . . . 10 (Ord 𝑗 → ((𝑗𝑆) ∩ {𝑗}) = ∅)
5953, 58syl 17 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∩ {𝑗}) = ∅)
60 nnord 7872 . . . . . . . . . . . 12 (𝑎 ∈ ω → Ord 𝑎)
61 ordirr 6381 . . . . . . . . . . . 12 (Ord 𝑎 → ¬ 𝑎𝑎)
6260, 61syl 17 . . . . . . . . . . 11 (𝑎 ∈ ω → ¬ 𝑎𝑎)
63 disjsn 4711 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎𝑎)
6462, 63sylibr 233 . . . . . . . . . 10 (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
6564ad2antrr 725 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66 unen 9064 . . . . . . . . 9 ((((𝑗𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
6746, 49, 59, 65, 66syl22anc 838 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68 simprr 772 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑏𝑆)
69 simplrl 776 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ ω)
7069, 23sstrdi 3990 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ On)
71 ordsuc 7810 . . . . . . . . . . . . . . . . . 18 (Ord 𝑗 ↔ Ord suc 𝑗)
7253, 71sylib 217 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord suc 𝑗)
7372adantrr 716 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → Ord suc 𝑗)
74 simp2 1135 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
7574ssdifssd 4138 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76 simpl1 1189 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏𝑆)
77 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
7876, 77eldifd 3955 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
7978ex 412 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80 onnmin 7795 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 (𝑆 ∖ suc 𝑗))
8175, 79, 80syl6an 683 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 (𝑆 ∖ suc 𝑗)))
8281con4d 115 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
8382imp 406 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84 simp3 1136 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85 ordsucss 7815 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
8786imp 406 . . . . . . . . . . . . . . . . . . . 20 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
8887sscond 4137 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89 intss 4967 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
9088, 89syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
91 simpl2 1190 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92 ordelon 6387 . . . . . . . . . . . . . . . . . . . 20 ((Ord suc 𝑗𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
9384, 92sylan 579 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94 onmindif 6455 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 (𝑆 ∖ suc 𝑏))
9591, 93, 94syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑏))
9690, 95sseldd 3979 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑗))
9783, 96impbida 800 . . . . . . . . . . . . . . . 16 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
9868, 70, 73, 97syl3anc 1369 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99 df-suc 6369 . . . . . . . . . . . . . . . 16 suc 𝑗 = (𝑗 ∪ {𝑗})
10099eleq2i 2820 . . . . . . . . . . . . . . 15 (𝑏 ∈ suc 𝑗𝑏 ∈ (𝑗 ∪ {𝑗}))
10198, 100bitrdi 287 . . . . . . . . . . . . . 14 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102101expr 456 . . . . . . . . . . . . 13 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏𝑆 → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103102pm5.32rd 577 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆)))
104 elin 3960 . . . . . . . . . . . 12 (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆))
105 elin 3960 . . . . . . . . . . . 12 (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆))
106103, 104, 1053bitr4g 314 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107106eqrdv 2725 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108 indir 4271 . . . . . . . . . 10 ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆))
109107, 108eqtrdi 2783 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)))
110 snssi 4807 . . . . . . . . . . . 12 (𝑗𝑆 → {𝑗} ⊆ 𝑆)
111 df-ss 3961 . . . . . . . . . . . 12 ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112110, 111sylib 217 . . . . . . . . . . 11 (𝑗𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113112uneq2d 4159 . . . . . . . . . 10 (𝑗𝑆 → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
114113ad2antrl 727 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
115109, 114eqtrd 2767 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ {𝑗}))
116 df-suc 6369 . . . . . . . . 9 suc 𝑎 = (𝑎 ∪ {𝑎})
117116a1i 11 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
11867, 115, 1173brtr4d 5174 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119 ineq1 4201 . . . . . . . . 9 (𝑏 = (𝑆 ∖ suc 𝑗) → (𝑏𝑆) = ( (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120119breq1d 5152 . . . . . . . 8 (𝑏 = (𝑆 ∖ suc 𝑗) → ((𝑏𝑆) ≈ suc 𝑎 ↔ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121120rspcev 3607 . . . . . . 7 (( (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
12245, 118, 121syl2anc 583 . . . . . 6 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
123122rexlimdvaa 3151 . . . . 5 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎))
124 ineq1 4201 . . . . . . 7 (𝑏 = 𝑗 → (𝑏𝑆) = (𝑗𝑆))
125124breq1d 5152 . . . . . 6 (𝑏 = 𝑗 → ((𝑏𝑆) ≈ suc 𝑎 ↔ (𝑗𝑆) ≈ suc 𝑎))
126125cbvrexvw 3230 . . . . 5 (∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)
127123, 126imbitrdi 250 . . . 4 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
128127ex 412 . . 3 (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)))
1292, 4, 6, 21, 128finds2 7900 . 2 (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
130129impcom 407 1 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2935  wrex 3065  Vcvv 3469  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4318  {csn 4624   cint 4944   class class class wbr 5142  Ord word 6362  Oncon0 6363  suc csuc 6365  ωcom 7864  cen 8954  Fincfn 8957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-om 7865  df-1o 8480  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961
This theorem is referenced by:  fin23lem23  10343
  Copyright terms: Public domain W3C validator