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

Theorem fin23lem26 10363
Description: Lemma for fin23lem22 10365. (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 5152 . . . 4 (𝑖 = ∅ → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ ∅))
21rexbidv 3177 . . 3 (𝑖 = ∅ → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ ∅))
3 breq2 5152 . . . 4 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
43rexbidv 3177 . . 3 (𝑖 = 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
5 breq2 5152 . . . 4 (𝑖 = suc 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ suc 𝑎))
65rexbidv 3177 . . 3 (𝑖 = suc 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
7 ordom 7897 . . . . 5 Ord ω
8 simpl 482 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9 0fi 9081 . . . . . . . 8 ∅ ∈ Fin
10 eleq1 2827 . . . . . . . 8 (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
119, 10mpbiri 258 . . . . . . 7 (𝑆 = ∅ → 𝑆 ∈ Fin)
1211necon3bi 2965 . . . . . 6 𝑆 ∈ Fin → 𝑆 ≠ ∅)
1312adantl 481 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14 tz7.5 6407 . . . . 5 ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
157, 8, 13, 14mp3an2i 1465 . . . 4 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
16 en0 9057 . . . . . 6 ((𝑗𝑆) ≈ ∅ ↔ (𝑗𝑆) = ∅)
17 incom 4217 . . . . . . 7 (𝑗𝑆) = (𝑆𝑗)
1817eqeq1i 2740 . . . . . 6 ((𝑗𝑆) = ∅ ↔ (𝑆𝑗) = ∅)
1916, 18bitri 275 . . . . 5 ((𝑗𝑆) ≈ ∅ ↔ (𝑆𝑗) = ∅)
2019rexbii 3092 . . . 4 (∃𝑗𝑆 (𝑗𝑆) ≈ ∅ ↔ ∃𝑗𝑆 (𝑆𝑗) = ∅)
2115, 20sylibr 234 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ ∅)
22 simplrl 777 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23 omsson 7891 . . . . . . . . . . 11 ω ⊆ On
2422, 23sstrdi 4008 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
2524ssdifssd 4157 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26 simplr 769 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ∈ Fin)
27 ssel2 3990 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → 𝑗 ∈ ω)
28 onfin2 9266 . . . . . . . . . . . . . . . . 17 ω = (On ∩ Fin)
29 inss2 4246 . . . . . . . . . . . . . . . . 17 (On ∩ Fin) ⊆ Fin
3028, 29eqsstri 4030 . . . . . . . . . . . . . . . 16 ω ⊆ Fin
31 peano2 7913 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
3230, 31sselid 3993 . . . . . . . . . . . . . . 15 (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
3327, 32syl 17 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
3433adantlr 715 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
35 ssfi 9212 . . . . . . . . . . . . . 14 ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
3635ex 412 . . . . . . . . . . . . 13 (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3734, 36syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3826, 37mtod 198 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39 ssdif0 4372 . . . . . . . . . . . 12 (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
4039necon3bbii 2986 . . . . . . . . . . 11 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
4138, 40sylib 218 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
4241ad2ant2lr 748 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43 onint 7810 . . . . . . . . 9 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4425, 42, 43syl2anc 584 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4544eldifad 3975 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46 simprr 773 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑗𝑆) ≈ 𝑎)
47 en2sn 9080 . . . . . . . . . . 11 ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
4847el2v 3485 . . . . . . . . . 10 {𝑗} ≈ {𝑎}
4948a1i 11 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50 simprl 771 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗𝑆)
5122, 50sseldd 3996 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52 nnord 7895 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
5351, 52syl 17 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord 𝑗)
54 ordirr 6404 . . . . . . . . . . . 12 (Ord 𝑗 → ¬ 𝑗𝑗)
55 elinel1 4211 . . . . . . . . . . . 12 (𝑗 ∈ (𝑗𝑆) → 𝑗𝑗)
5654, 55nsyl 140 . . . . . . . . . . 11 (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗𝑆))
57 disjsn 4716 . . . . . . . . . . 11 (((𝑗𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗𝑆))
5856, 57sylibr 234 . . . . . . . . . 10 (Ord 𝑗 → ((𝑗𝑆) ∩ {𝑗}) = ∅)
5953, 58syl 17 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∩ {𝑗}) = ∅)
60 nnord 7895 . . . . . . . . . . . 12 (𝑎 ∈ ω → Ord 𝑎)
61 ordirr 6404 . . . . . . . . . . . 12 (Ord 𝑎 → ¬ 𝑎𝑎)
6260, 61syl 17 . . . . . . . . . . 11 (𝑎 ∈ ω → ¬ 𝑎𝑎)
63 disjsn 4716 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎𝑎)
6462, 63sylibr 234 . . . . . . . . . 10 (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
6564ad2antrr 726 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66 unen 9085 . . . . . . . . 9 ((((𝑗𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
6746, 49, 59, 65, 66syl22anc 839 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68 simprr 773 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑏𝑆)
69 simplrl 777 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ ω)
7069, 23sstrdi 4008 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ On)
71 ordsuc 7833 . . . . . . . . . . . . . . . . . 18 (Ord 𝑗 ↔ Ord suc 𝑗)
7253, 71sylib 218 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord suc 𝑗)
7372adantrr 717 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → Ord suc 𝑗)
74 simp2 1136 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
7574ssdifssd 4157 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76 simpl1 1190 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏𝑆)
77 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
7876, 77eldifd 3974 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
7978ex 412 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80 onnmin 7818 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 (𝑆 ∖ suc 𝑗))
8175, 79, 80syl6an 684 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 (𝑆 ∖ suc 𝑗)))
8281con4d 115 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
8382imp 406 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84 simp3 1137 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85 ordsucss 7838 . . . . . . . . . . . . . . . . . . . . . 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 4156 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89 intss 4974 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
9088, 89syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
91 simpl2 1191 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92 ordelon 6410 . . . . . . . . . . . . . . . . . . . 20 ((Ord suc 𝑗𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
9384, 92sylan 580 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94 onmindif 6478 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 (𝑆 ∖ suc 𝑏))
9591, 93, 94syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑏))
9690, 95sseldd 3996 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑗))
9783, 96impbida 801 . . . . . . . . . . . . . . . 16 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
9868, 70, 73, 97syl3anc 1370 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99 df-suc 6392 . . . . . . . . . . . . . . . 16 suc 𝑗 = (𝑗 ∪ {𝑗})
10099eleq2i 2831 . . . . . . . . . . . . . . 15 (𝑏 ∈ suc 𝑗𝑏 ∈ (𝑗 ∪ {𝑗}))
10198, 100bitrdi 287 . . . . . . . . . . . . . 14 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102101expr 456 . . . . . . . . . . . . 13 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏𝑆 → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103102pm5.32rd 578 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆)))
104 elin 3979 . . . . . . . . . . . 12 (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆))
105 elin 3979 . . . . . . . . . . . 12 (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆))
106103, 104, 1053bitr4g 314 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107106eqrdv 2733 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108 indir 4292 . . . . . . . . . 10 ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆))
109107, 108eqtrdi 2791 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)))
110 snssi 4813 . . . . . . . . . . . 12 (𝑗𝑆 → {𝑗} ⊆ 𝑆)
111 dfss2 3981 . . . . . . . . . . . 12 ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112110, 111sylib 218 . . . . . . . . . . 11 (𝑗𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113112uneq2d 4178 . . . . . . . . . 10 (𝑗𝑆 → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
114113ad2antrl 728 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
115109, 114eqtrd 2775 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ {𝑗}))
116 df-suc 6392 . . . . . . . . 9 suc 𝑎 = (𝑎 ∪ {𝑎})
117116a1i 11 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
11867, 115, 1173brtr4d 5180 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119 ineq1 4221 . . . . . . . . 9 (𝑏 = (𝑆 ∖ suc 𝑗) → (𝑏𝑆) = ( (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120119breq1d 5158 . . . . . . . 8 (𝑏 = (𝑆 ∖ suc 𝑗) → ((𝑏𝑆) ≈ suc 𝑎 ↔ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121120rspcev 3622 . . . . . . 7 (( (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
12245, 118, 121syl2anc 584 . . . . . 6 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
123122rexlimdvaa 3154 . . . . 5 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎))
124 ineq1 4221 . . . . . . 7 (𝑏 = 𝑗 → (𝑏𝑆) = (𝑗𝑆))
125124breq1d 5158 . . . . . 6 (𝑏 = 𝑗 → ((𝑏𝑆) ≈ suc 𝑎 ↔ (𝑗𝑆) ≈ suc 𝑎))
126125cbvrexvw 3236 . . . . 5 (∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)
127123, 126imbitrdi 251 . . . 4 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
128127ex 412 . . 3 (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)))
1292, 4, 6, 21, 128finds2 7921 . 2 (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
130129impcom 407 1 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wrex 3068  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  {csn 4631   cint 4951   class class class wbr 5148  Ord word 6385  Oncon0 6386  suc csuc 6388  ωcom 7887  cen 8981  Fincfn 8984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-om 7888  df-1o 8505  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988
This theorem is referenced by:  fin23lem23  10364
  Copyright terms: Public domain W3C validator