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

Theorem fin23lem26 9098
Description: Lemma for fin23lem22 9100. (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 4622 . . . 4 (𝑖 = ∅ → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ ∅))
21rexbidv 3046 . . 3 (𝑖 = ∅ → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ ∅))
3 breq2 4622 . . . 4 (𝑖 = 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ 𝑎))
43rexbidv 3046 . . 3 (𝑖 = 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎))
5 breq2 4622 . . . 4 (𝑖 = suc 𝑎 → ((𝑗𝑆) ≈ 𝑖 ↔ (𝑗𝑆) ≈ suc 𝑎))
65rexbidv 3046 . . 3 (𝑖 = suc 𝑎 → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
7 ordom 7028 . . . . . 6 Ord ω
87a1i 11 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → Ord ω)
9 simpl 473 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ⊆ ω)
10 0fin 8139 . . . . . . . 8 ∅ ∈ Fin
11 eleq1 2686 . . . . . . . 8 (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅ ∈ Fin))
1210, 11mpbiri 248 . . . . . . 7 (𝑆 = ∅ → 𝑆 ∈ Fin)
1312necon3bi 2816 . . . . . 6 𝑆 ∈ Fin → 𝑆 ≠ ∅)
1413adantl 482 . . . . 5 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝑆 ≠ ∅)
15 tz7.5 5708 . . . . 5 ((Ord ω ∧ 𝑆 ⊆ ω ∧ 𝑆 ≠ ∅) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
168, 9, 14, 15syl3anc 1323 . . . 4 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑆𝑗) = ∅)
17 en0 7970 . . . . . 6 ((𝑗𝑆) ≈ ∅ ↔ (𝑗𝑆) = ∅)
18 incom 3788 . . . . . . 7 (𝑗𝑆) = (𝑆𝑗)
1918eqeq1i 2626 . . . . . 6 ((𝑗𝑆) = ∅ ↔ (𝑆𝑗) = ∅)
2017, 19bitri 264 . . . . 5 ((𝑗𝑆) ≈ ∅ ↔ (𝑆𝑗) = ∅)
2120rexbii 3035 . . . 4 (∃𝑗𝑆 (𝑗𝑆) ≈ ∅ ↔ ∃𝑗𝑆 (𝑆𝑗) = ∅)
2216, 21sylibr 224 . . 3 ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ ∅)
23 simplrl 799 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω)
24 omsson 7023 . . . . . . . . . . 11 ω ⊆ On
2523, 24syl6ss 3599 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑆 ⊆ On)
2625ssdifssd 3731 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On)
27 simplr 791 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ∈ Fin)
28 ssel2 3582 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → 𝑗 ∈ ω)
29 onfin2 8103 . . . . . . . . . . . . . . . . 17 ω = (On ∩ Fin)
30 inss2 3817 . . . . . . . . . . . . . . . . 17 (On ∩ Fin) ⊆ Fin
3129, 30eqsstri 3619 . . . . . . . . . . . . . . . 16 ω ⊆ Fin
32 peano2 7040 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
3331, 32sseldi 3585 . . . . . . . . . . . . . . 15 (𝑗 ∈ ω → suc 𝑗 ∈ Fin)
3428, 33syl 17 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ω ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
3534adantlr 750 . . . . . . . . . . . . 13 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → suc 𝑗 ∈ Fin)
36 ssfi 8131 . . . . . . . . . . . . . 14 ((suc 𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin)
3736ex 450 . . . . . . . . . . . . 13 (suc 𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3835, 37syl 17 . . . . . . . . . . . 12 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ⊆ suc 𝑗𝑆 ∈ Fin))
3927, 38mtod 189 . . . . . . . . . . 11 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → ¬ 𝑆 ⊆ suc 𝑗)
40 ssdif0 3921 . . . . . . . . . . . 12 (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅)
4140necon3bbii 2837 . . . . . . . . . . 11 𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅)
4239, 41sylib 208 . . . . . . . . . 10 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑗𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅)
4342ad2ant2lr 783 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅)
44 onint 6949 . . . . . . . . 9 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4526, 43, 44syl2anc 692 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗))
4645eldifad 3571 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ∈ 𝑆)
47 simprr 795 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑗𝑆) ≈ 𝑎)
48 vex 3192 . . . . . . . . . . 11 𝑗 ∈ V
49 vex 3192 . . . . . . . . . . 11 𝑎 ∈ V
50 en2sn 7988 . . . . . . . . . . 11 ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎})
5148, 49, 50mp2an 707 . . . . . . . . . 10 {𝑗} ≈ {𝑎}
5251a1i 11 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎})
53 simprl 793 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗𝑆)
5423, 53sseldd 3588 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → 𝑗 ∈ ω)
55 nnord 7027 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
5654, 55syl 17 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord 𝑗)
57 ordirr 5705 . . . . . . . . . . . 12 (Ord 𝑗 → ¬ 𝑗𝑗)
58 inss1 3816 . . . . . . . . . . . . 13 (𝑗𝑆) ⊆ 𝑗
5958sseli 3583 . . . . . . . . . . . 12 (𝑗 ∈ (𝑗𝑆) → 𝑗𝑗)
6057, 59nsyl 135 . . . . . . . . . . 11 (Ord 𝑗 → ¬ 𝑗 ∈ (𝑗𝑆))
61 disjsn 4221 . . . . . . . . . . 11 (((𝑗𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗𝑆))
6260, 61sylibr 224 . . . . . . . . . 10 (Ord 𝑗 → ((𝑗𝑆) ∩ {𝑗}) = ∅)
6356, 62syl 17 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∩ {𝑗}) = ∅)
64 nnord 7027 . . . . . . . . . . . 12 (𝑎 ∈ ω → Ord 𝑎)
65 ordirr 5705 . . . . . . . . . . . 12 (Ord 𝑎 → ¬ 𝑎𝑎)
6664, 65syl 17 . . . . . . . . . . 11 (𝑎 ∈ ω → ¬ 𝑎𝑎)
67 disjsn 4221 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎𝑎)
6866, 67sylibr 224 . . . . . . . . . 10 (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅)
6968ad2antrr 761 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅)
70 unen 7991 . . . . . . . . 9 ((((𝑗𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
7147, 52, 63, 69, 70syl22anc 1324 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎}))
72 simprr 795 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑏𝑆)
73 simplrl 799 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ ω)
7473, 24syl6ss 3599 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → 𝑆 ⊆ On)
75 ordsuc 6968 . . . . . . . . . . . . . . . . . 18 (Ord 𝑗 ↔ Ord suc 𝑗)
7656, 75sylib 208 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → Ord suc 𝑗)
7776adantrr 752 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → Ord suc 𝑗)
78 simp2 1060 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On)
7978ssdifssd 3731 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On)
80 simpl1 1062 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏𝑆)
81 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗)
8280, 81eldifd 3570 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗))
8382ex 450 . . . . . . . . . . . . . . . . . . . 20 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗𝑏 ∈ (𝑆 ∖ suc 𝑗)))
84 onnmin 6957 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 (𝑆 ∖ suc 𝑗))
8579, 83, 84syl6an 567 . . . . . . . . . . . . . . . . . . 19 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 (𝑆 ∖ suc 𝑗)))
8685con4d 114 . . . . . . . . . . . . . . . . . 18 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗))
8786imp 445 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗)
88 simp3 1061 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗)
89 ordsucss 6972 . . . . . . . . . . . . . . . . . . . . . 22 (Ord suc 𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗))
9190imp 445 . . . . . . . . . . . . . . . . . . . 20 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗)
9291sscond 3730 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏))
93 intss 4468 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
9492, 93syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑏) ⊆ (𝑆 ∖ suc 𝑗))
95 simpl2 1063 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On)
96 ordelon 5711 . . . . . . . . . . . . . . . . . . . 20 ((Ord suc 𝑗𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
9788, 96sylan 488 . . . . . . . . . . . . . . . . . . 19 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On)
98 onmindif 5779 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 (𝑆 ∖ suc 𝑏))
9995, 97, 98syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑏))
10094, 99sseldd 3588 . . . . . . . . . . . . . . . . 17 (((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 (𝑆 ∖ suc 𝑗))
10187, 100impbida 876 . . . . . . . . . . . . . . . 16 ((𝑏𝑆𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
10272, 74, 77, 101syl3anc 1323 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗))
103 df-suc 5693 . . . . . . . . . . . . . . . 16 suc 𝑗 = (𝑗 ∪ {𝑗})
104103eleq2i 2690 . . . . . . . . . . . . . . 15 (𝑏 ∈ suc 𝑗𝑏 ∈ (𝑗 ∪ {𝑗}))
105102, 104syl6bb 276 . . . . . . . . . . . . . 14 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ ((𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎) ∧ 𝑏𝑆)) → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))
106105expr 642 . . . . . . . . . . . . 13 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏𝑆 → (𝑏 (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))))
107106pm5.32rd 671 . . . . . . . . . . . 12 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆)))
108 elin 3779 . . . . . . . . . . . 12 (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 (𝑆 ∖ suc 𝑗) ∧ 𝑏𝑆))
109 elin 3779 . . . . . . . . . . . 12 (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏𝑆))
110107, 108, 1093bitr4g 303 . . . . . . . . . . 11 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → (𝑏 ∈ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆)))
111110eqrdv 2619 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆))
112 indir 3856 . . . . . . . . . 10 ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆))
113111, 112syl6eq 2671 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)))
114 snssi 4313 . . . . . . . . . . . 12 (𝑗𝑆 → {𝑗} ⊆ 𝑆)
115 df-ss 3573 . . . . . . . . . . . 12 ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗})
116114, 115sylib 208 . . . . . . . . . . 11 (𝑗𝑆 → ({𝑗} ∩ 𝑆) = {𝑗})
117116uneq2d 3750 . . . . . . . . . 10 (𝑗𝑆 → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
118117ad2antrl 763 . . . . . . . . 9 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ((𝑗𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗𝑆) ∪ {𝑗}))
119113, 118eqtrd 2655 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗𝑆) ∪ {𝑗}))
120 df-suc 5693 . . . . . . . . 9 suc 𝑎 = (𝑎 ∪ {𝑎})
121120a1i 11 . . . . . . . 8 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎}))
12271, 119, 1213brtr4d 4650 . . . . . . 7 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)
123 ineq1 3790 . . . . . . . . 9 (𝑏 = (𝑆 ∖ suc 𝑗) → (𝑏𝑆) = ( (𝑆 ∖ suc 𝑗) ∩ 𝑆))
124123breq1d 4628 . . . . . . . 8 (𝑏 = (𝑆 ∖ suc 𝑗) → ((𝑏𝑆) ≈ suc 𝑎 ↔ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎))
125124rspcev 3298 . . . . . . 7 (( (𝑆 ∖ suc 𝑗) ∈ 𝑆 ∧ ( (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
12646, 122, 125syl2anc 692 . . . . . 6 (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) ∧ (𝑗𝑆 ∧ (𝑗𝑆) ≈ 𝑎)) → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎)
127126rexlimdvaa 3026 . . . . 5 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎))
128 ineq1 3790 . . . . . . 7 (𝑏 = 𝑗 → (𝑏𝑆) = (𝑗𝑆))
129128breq1d 4628 . . . . . 6 (𝑏 = 𝑗 → ((𝑏𝑆) ≈ suc 𝑎 ↔ (𝑗𝑆) ≈ suc 𝑎))
130129cbvrexv 3163 . . . . 5 (∃𝑏𝑆 (𝑏𝑆) ≈ suc 𝑎 ↔ ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)
131127, 130syl6ib 241 . . . 4 ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin)) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎))
132131ex 450 . . 3 (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → (∃𝑗𝑆 (𝑗𝑆) ≈ 𝑎 → ∃𝑗𝑆 (𝑗𝑆) ≈ suc 𝑎)))
1332, 4, 6, 22, 132finds2 7048 . 2 (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖))
134133impcom 446 1 (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗𝑆 (𝑗𝑆) ≈ 𝑖)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wrex 2908  Vcvv 3189  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  {csn 4153   cint 4445   class class class wbr 4618  Ord word 5686  Oncon0 5687  suc csuc 5689  ωcom 7019  cen 7903  Fincfn 7906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-1o 7512  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910
This theorem is referenced by:  fin23lem23  9099
  Copyright terms: Public domain W3C validator