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

Theorem fin23lem26 9739
Description: Lemma for fin23lem22 9741. (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 5061 . . . 4 (𝑖 = ∅ → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ ∅))
21rexbidv 3295 . . 3 (𝑖 = ∅ → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ ∅))
3 breq2 5061 . . . 4 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
43rexbidv 3295 . . 3 (𝑖 = 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
5 breq2 5061 . . . 4 (𝑖 = suc 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ suc 𝑎))
65rexbidv 3295 . . 3 (𝑖 = suc 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
7 ordom 7581 . . . . 5 Ord ω
8 simpl 485 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
9 0fin 8738 . . . . . . . 8 ∅ ∈ Fin
10 eleq1 2898 . . . . . . . 8 (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
119, 10mpbiri 260 . . . . . . 7 (𝑆 = ∅ → 𝑆 ∈ Fin)
1211necon3bi 3040 . . . . . 6 𝑆 ∈ Fin → 𝑆 ≠ ∅)
1312adantl 484 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
14 tz7.5 6205 . . . . 5 ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
157, 8, 13, 14mp3an2i 1459 . . . 4 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
16 en0 8564 . . . . . 6 ((𝑗𝑆) ≈ ∅ ↔ (𝑗𝑆) = ∅)
17 incom 4176 . . . . . . 7 (𝑗𝑆) = (𝑆𝑗)
1817eqeq1i 2824 . . . . . 6 ((𝑗𝑆) = ∅ ↔ (𝑆𝑗) = ∅)
1916, 18bitri 277 . . . . 5 ((𝑗𝑆) ≈ ∅ ↔ (𝑆𝑗) = ∅)
2019rexbii 3245 . . . 4 (∃𝑗𝑆 (𝑗𝑆) ≈ ∅ ↔ ∃𝑗𝑆 (𝑆𝑗) = ∅)
2115, 20sylibr 236 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ ∅)
22 simplrl 775 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
23 omsson 7576 . . . . . . . . . . 11 ω ⊆ On
2422, 23sstrdi 3977 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
2524ssdifssd 4117 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
26 simplr 767 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ∈ Fin)
27 ssel2 3960 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → 𝑗 ∈ ω)
28 onfin2 8702 . . . . . . . . . . . . . . . . 17 ω = (On ∩ Fin)
29 inss2 4204 . . . . . . . . . . . . . . . . 17 (On ∩ Fin) ⊆ Fin
3028, 29eqsstri 3999 . . . . . . . . . . . . . . . 16 ω ⊆ Fin
31 peano2 7594 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
3230, 31sseldi 3963 . . . . . . . . . . . . . . 15 (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
3327, 32syl 17 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
3433adantlr 713 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
35 ssfi 8730 . . . . . . . . . . . . . 14 ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
3635ex 415 . . . . . . . . . . . . 13 (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3734, 36syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3826, 37mtod 200 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
39 ssdif0 4321 . . . . . . . . . . . 12 (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
4039necon3bbii 3061 . . . . . . . . . . 11 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
4138, 40sylib 220 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
4241ad2ant2lr 746 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
43 onint 7502 . . . . . . . . 9 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4425, 42, 43syl2anc 586 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4544eldifad 3946 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ 𝑆)
46 simprr 771 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑗𝑆) ≈ 𝑎)
47 en2sn 8585 . . . . . . . . . . 11 ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
4847el2v 3500 . . . . . . . . . 10 {𝑗} ≈ {𝑎}
4948a1i 11 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
50 simprl 769 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗𝑆)
5122, 50sseldd 3966 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
52 nnord 7580 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
5351, 52syl 17 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord 𝑗)
54 ordirr 6202 . . . . . . . . . . . 12 (Ord 𝑗 → ¬ 𝑗𝑗)
55 elinel1 4170 . . . . . . . . . . . 12 (𝑗 ∈ (𝑗𝑆) → 𝑗𝑗)
5654, 55nsyl 142 . . . . . . . . . . 11 (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗𝑆))
57 disjsn 4639 . . . . . . . . . . 11 (((𝑗𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗𝑆))
5856, 57sylibr 236 . . . . . . . . . 10 (Ord 𝑗 → ((𝑗𝑆) ∩ {𝑗}) = ∅)
5953, 58syl 17 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∩ {𝑗}) = ∅)
60 nnord 7580 . . . . . . . . . . . 12 (𝑎 ∈ ω → Ord 𝑎)
61 ordirr 6202 . . . . . . . . . . . 12 (Ord 𝑎 → ¬ 𝑎𝑎)
6260, 61syl 17 . . . . . . . . . . 11 (𝑎 ∈ ω → ¬ 𝑎𝑎)
63 disjsn 4639 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎𝑎)
6462, 63sylibr 236 . . . . . . . . . 10 (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
6564ad2antrr 724 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
66 unen 8588 . . . . . . . . 9 ((((𝑗𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
6746, 49, 59, 65, 66syl22anc 836 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
68 simprr 771 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑏𝑆)
69 simplrl 775 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ ω)
7069, 23sstrdi 3977 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ On)
71 ordsuc 7521 . . . . . . . . . . . . . . . . . 18 (Ord 𝑗 ↔ Ord suc 𝑗)
7253, 71sylib 220 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord suc 𝑗)
7372adantrr 715 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → Ord suc 𝑗)
74 simp2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
7574ssdifssd 4117 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
76 simpl1 1185 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏𝑆)
77 simpr 487 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
7876, 77eldifd 3945 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
7978ex 415 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗𝑏 ∈ (𝑆 ∖ suc 𝑗)))
80 onnmin 7510 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 (𝑆 ∖ suc 𝑗))
8175, 79, 80syl6an 682 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 (𝑆 ∖ suc 𝑗)))
8281con4d 115 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
8382imp 409 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
84 simp3 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
85 ordsucss 7525 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
8786imp 409 . . . . . . . . . . . . . . . . . . . 20 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
8887sscond 4116 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
89 intss 4888 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
9088, 89syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
91 simpl2 1186 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
92 ordelon 6208 . . . . . . . . . . . . . . . . . . . 20 ((Ord suc 𝑗𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
9384, 92sylan 582 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
94 onmindif 6273 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 (𝑆 ∖ suc 𝑏))
9591, 93, 94syl2anc 586 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑏))
9690, 95sseldd 3966 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑗))
9783, 96impbida 799 . . . . . . . . . . . . . . . 16 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
9868, 70, 73, 97syl3anc 1365 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
99 df-suc 6190 . . . . . . . . . . . . . . . 16 suc 𝑗 = (𝑗 ∪ {𝑗})
10099eleq2i 2902 . . . . . . . . . . . . . . 15 (𝑏 ∈ suc 𝑗𝑏 ∈ (𝑗 ∪ {𝑗}))
10198, 100syl6bb 289 . . . . . . . . . . . . . 14 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
102101expr 459 . . . . . . . . . . . . 13 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏𝑆 → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
103102pm5.32rd 580 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆)))
104 elin 4167 . . . . . . . . . . . 12 (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆))
105 elin 4167 . . . . . . . . . . . 12 (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆))
106103, 104, 1053bitr4g 316 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
107106eqrdv 2817 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
108 indir 4250 . . . . . . . . . 10 ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆))
109107, 108syl6eq 2870 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)))
110 snssi 4733 . . . . . . . . . . . 12 (𝑗𝑆 → {𝑗} ⊆ 𝑆)
111 df-ss 3950 . . . . . . . . . . . 12 ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
112110, 111sylib 220 . . . . . . . . . . 11 (𝑗𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
113112uneq2d 4137 . . . . . . . . . 10 (𝑗𝑆 → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
114113ad2antrl 726 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
115109, 114eqtrd 2854 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ {𝑗}))
116 df-suc 6190 . . . . . . . . 9 suc 𝑎 = (𝑎 ∪ {𝑎})
117116a1i 11 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
11867, 115, 1173brtr4d 5089 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
119 ineq1 4179 . . . . . . . . 9 (𝑏 = (𝑆 ∖ suc 𝑗) → (𝑏𝑆) = ( (𝑆 ∖ suc 𝑗) ∩ 𝑆))
120119breq1d 5067 . . . . . . . 8 (𝑏 = (𝑆 ∖ suc 𝑗) → ((𝑏𝑆) ≈ suc 𝑎 ↔ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
121120rspcev 3621 . . . . . . 7 (( (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
12245, 118, 121syl2anc 586 . . . . . 6 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
123122rexlimdvaa 3283 . . . . 5 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎))
124 ineq1 4179 . . . . . . 7 (𝑏 = 𝑗 → (𝑏𝑆) = (𝑗𝑆))
125124breq1d 5067 . . . . . 6 (𝑏 = 𝑗 → ((𝑏𝑆) ≈ suc 𝑎 ↔ (𝑗𝑆) ≈ suc 𝑎))
126125cbvrexvw 3449 . . . . 5 (∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)
127123, 126syl6ib 253 . . . 4 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
128127ex 415 . . 3 (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)))
1292, 4, 6, 21, 128finds2 7602 . 2 (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
130129impcom 410 1 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  w3a 1081   = wceq 1530  wcel 2107  wne 3014  wrex 3137  Vcvv 3493  cdif 3931  cun 3932  cin 3933  wss 3934  c0 4289  {csn 4559   cint 4867   class class class wbr 5057  Ord word 6183  Oncon0 6184  suc csuc 6186  ωcom 7572  cen 8498  Fincfn 8501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-br 5058  df-opab 5120  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7573  df-1o 8094  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505
This theorem is referenced by:  fin23lem23  9740
  Copyright terms: Public domain W3C validator