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

Theorem fiint 9366
Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of 𝐴 is in 𝐴". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.) Use a separate setvar for the right-hand side and avoid ax-pow 5365. (Revised by BTernaryTau, 14-Jan-2025.)
Assertion
Ref Expression
fiint (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑧,𝐴

Proof of Theorem fiint
Dummy variables 𝑣 𝑢 𝑡 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 9016 . . . . . . 7 (𝑧 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑧𝑤)
2 nnfi 9207 . . . . . . . . . 10 (𝑤 ∈ ω → 𝑤 ∈ Fin)
3 ensymfib 9224 . . . . . . . . . 10 (𝑤 ∈ Fin → (𝑤𝑧𝑧𝑤))
42, 3syl 17 . . . . . . . . 9 (𝑤 ∈ ω → (𝑤𝑧𝑧𝑤))
5 breq1 5146 . . . . . . . . . . . . . . . 16 (𝑤 = ∅ → (𝑤𝑧 ↔ ∅ ≈ 𝑧))
65anbi2d 630 . . . . . . . . . . . . . . 15 (𝑤 = ∅ → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) ↔ ((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧)))
76imbi1d 341 . . . . . . . . . . . . . 14 (𝑤 = ∅ → ((((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) ↔ (((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → 𝑧𝐴)))
87albidv 1920 . . . . . . . . . . . . 13 (𝑤 = ∅ → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) ↔ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → 𝑧𝐴)))
9 breq1 5146 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑡 → (𝑤𝑧𝑡𝑧))
109anbi2d 630 . . . . . . . . . . . . . . 15 (𝑤 = 𝑡 → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) ↔ ((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧)))
1110imbi1d 341 . . . . . . . . . . . . . 14 (𝑤 = 𝑡 → ((((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) ↔ (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴)))
1211albidv 1920 . . . . . . . . . . . . 13 (𝑤 = 𝑡 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) ↔ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴)))
13 breq1 5146 . . . . . . . . . . . . . . . 16 (𝑤 = suc 𝑡 → (𝑤𝑧 ↔ suc 𝑡𝑧))
1413anbi2d 630 . . . . . . . . . . . . . . 15 (𝑤 = suc 𝑡 → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) ↔ ((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧)))
1514imbi1d 341 . . . . . . . . . . . . . 14 (𝑤 = suc 𝑡 → ((((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) ↔ (((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧) → 𝑧𝐴)))
1615albidv 1920 . . . . . . . . . . . . 13 (𝑤 = suc 𝑡 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) ↔ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧) → 𝑧𝐴)))
17 en0r 9060 . . . . . . . . . . . . . . . . . . . 20 (∅ ≈ 𝑧𝑧 = ∅)
1817biimpi 216 . . . . . . . . . . . . . . . . . . 19 (∅ ≈ 𝑧𝑧 = ∅)
1918anim1i 615 . . . . . . . . . . . . . . . . . 18 ((∅ ≈ 𝑧𝑧 ≠ ∅) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
2019ancoms 458 . . . . . . . . . . . . . . . . 17 ((𝑧 ≠ ∅ ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
2120adantll 714 . . . . . . . . . . . . . . . 16 (((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → (𝑧 = ∅ ∧ 𝑧 ≠ ∅))
22 df-ne 2941 . . . . . . . . . . . . . . . . 17 (𝑧 ≠ ∅ ↔ ¬ 𝑧 = ∅)
23 pm3.24 402 . . . . . . . . . . . . . . . . . 18 ¬ (𝑧 = ∅ ∧ ¬ 𝑧 = ∅)
2423pm2.21i 119 . . . . . . . . . . . . . . . . 17 ((𝑧 = ∅ ∧ ¬ 𝑧 = ∅) → 𝑧𝐴)
2522, 24sylan2b 594 . . . . . . . . . . . . . . . 16 ((𝑧 = ∅ ∧ 𝑧 ≠ ∅) → 𝑧𝐴)
2621, 25syl 17 . . . . . . . . . . . . . . 15 (((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → 𝑧𝐴)
2726ax-gen 1795 . . . . . . . . . . . . . 14 𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → 𝑧𝐴)
2827a1i 11 . . . . . . . . . . . . 13 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ ∅ ≈ 𝑧) → 𝑧𝐴))
29 nfv 1914 . . . . . . . . . . . . . . 15 𝑧𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴
30 nfa1 2151 . . . . . . . . . . . . . . 15 𝑧𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴)
31 bren 8995 . . . . . . . . . . . . . . . . . . 19 (suc 𝑡𝑧 ↔ ∃𝑓 𝑓:suc 𝑡1-1-onto𝑧)
32 ssel 3977 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝐴 → ((𝑓𝑡) ∈ 𝑧 → (𝑓𝑡) ∈ 𝐴))
33 f1of 6848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑡1-1-onto𝑧𝑓:suc 𝑡𝑧)
34 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡 ∈ V
3534sucid 6466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ∈ suc 𝑡
36 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:suc 𝑡𝑧𝑡 ∈ suc 𝑡) → (𝑓𝑡) ∈ 𝑧)
3733, 35, 36sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑡1-1-onto𝑧 → (𝑓𝑡) ∈ 𝑧)
3832, 37impel 505 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) → (𝑓𝑡) ∈ 𝐴)
3938adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → (𝑓𝑡) ∈ 𝐴)
40 df-ne 2941 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑡) ≠ ∅ ↔ ¬ (𝑓𝑡) = ∅)
41 imassrn 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓𝑡) ⊆ ran 𝑓
42 dff1o2 6853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑡1-1-onto𝑧 ↔ (𝑓 Fn suc 𝑡 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑧))
4342simp3bi 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑡1-1-onto𝑧 → ran 𝑓 = 𝑧)
4441, 43sseqtrid 4026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑡1-1-onto𝑧 → (𝑓𝑡) ⊆ 𝑧)
45 sstr2 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑓𝑡) ⊆ 𝑧 → (𝑧𝐴 → (𝑓𝑡) ⊆ 𝐴))
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑡1-1-onto𝑧 → (𝑧𝐴 → (𝑓𝑡) ⊆ 𝐴))
4746anim1d 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:suc 𝑡1-1-onto𝑧 → ((𝑧𝐴 ∧ (𝑓𝑡) ≠ ∅) → ((𝑓𝑡) ⊆ 𝐴 ∧ (𝑓𝑡) ≠ ∅)))
48 f1of1 6847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑡1-1-onto𝑧𝑓:suc 𝑡1-1𝑧)
49 sssucid 6464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑡 ⊆ suc 𝑡
50 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑓 ∈ V
51 f1imaen3g 9056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑓:suc 𝑡1-1𝑧𝑡 ⊆ suc 𝑡𝑓 ∈ V) → 𝑡 ≈ (𝑓𝑡))
5249, 50, 51mp3an23 1455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑡1-1𝑧𝑡 ≈ (𝑓𝑡))
5348, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:suc 𝑡1-1-onto𝑧𝑡 ≈ (𝑓𝑡))
5447, 53jctird 526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:suc 𝑡1-1-onto𝑧 → ((𝑧𝐴 ∧ (𝑓𝑡) ≠ ∅) → (((𝑓𝑡) ⊆ 𝐴 ∧ (𝑓𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓𝑡))))
5550imaex 7936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓𝑡) ∈ V
56 sseq1 4009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑡) → (𝑧𝐴 ↔ (𝑓𝑡) ⊆ 𝐴))
57 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑡) → (𝑧 ≠ ∅ ↔ (𝑓𝑡) ≠ ∅))
5856, 57anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑡) → ((𝑧𝐴𝑧 ≠ ∅) ↔ ((𝑓𝑡) ⊆ 𝐴 ∧ (𝑓𝑡) ≠ ∅)))
59 breq2 5147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑡) → (𝑡𝑧𝑡 ≈ (𝑓𝑡)))
6058, 59anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑡) → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) ↔ (((𝑓𝑡) ⊆ 𝐴 ∧ (𝑓𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓𝑡))))
61 inteq 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑡) → 𝑧 = (𝑓𝑡))
6261eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑓𝑡) → ( 𝑧𝐴 (𝑓𝑡) ∈ 𝐴))
6360, 62imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑓𝑡) → ((((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ↔ ((((𝑓𝑡) ⊆ 𝐴 ∧ (𝑓𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓𝑡)) → (𝑓𝑡) ∈ 𝐴)))
6455, 63spcv 3605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → ((((𝑓𝑡) ⊆ 𝐴 ∧ (𝑓𝑡) ≠ ∅) ∧ 𝑡 ≈ (𝑓𝑡)) → (𝑓𝑡) ∈ 𝐴))
6554, 64sylan9 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓:suc 𝑡1-1-onto𝑧 ∧ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴)) → ((𝑧𝐴 ∧ (𝑓𝑡) ≠ ∅) → (𝑓𝑡) ∈ 𝐴))
66 ineq1 4213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 = (𝑓𝑡) → (𝑣𝑢) = ( (𝑓𝑡) ∩ 𝑢))
6766eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 = (𝑓𝑡) → ((𝑣𝑢) ∈ 𝐴 ↔ ( (𝑓𝑡) ∩ 𝑢) ∈ 𝐴))
68 ineq2 4214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 = (𝑓𝑡) → ( (𝑓𝑡) ∩ 𝑢) = ( (𝑓𝑡) ∩ (𝑓𝑡)))
6968eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 = (𝑓𝑡) → (( (𝑓𝑡) ∩ 𝑢) ∈ 𝐴 ↔ ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))
7067, 69rspc2v 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( (𝑓𝑡) ∈ 𝐴 ∧ (𝑓𝑡) ∈ 𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))
7170ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ( (𝑓𝑡) ∈ 𝐴 → ((𝑓𝑡) ∈ 𝐴 → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴)))
7265, 71syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓:suc 𝑡1-1-onto𝑧 ∧ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴)) → ((𝑧𝐴 ∧ (𝑓𝑡) ≠ ∅) → ((𝑓𝑡) ∈ 𝐴 → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))))
7372com4r 94 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ((𝑓:suc 𝑡1-1-onto𝑧 ∧ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴)) → ((𝑧𝐴 ∧ (𝑓𝑡) ≠ ∅) → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))))
7473exp5c 444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → (𝑓:suc 𝑡1-1-onto𝑧 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (𝑧𝐴 → ((𝑓𝑡) ≠ ∅ → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))))))
7574com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝐴 → (𝑓:suc 𝑡1-1-onto𝑧 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ((𝑓𝑡) ≠ ∅ → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))))))
7675imp43 427 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → ((𝑓𝑡) ≠ ∅ → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴)))
7740, 76biimtrrid 243 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → (¬ (𝑓𝑡) = ∅ → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴)))
78 inteq 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑡) = ∅ → (𝑓𝑡) = ∅)
79 int0 4962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ∅ = V
8078, 79eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑡) = ∅ → (𝑓𝑡) = V)
8180ineq1d 4219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑡) = ∅ → ( (𝑓𝑡) ∩ (𝑓𝑡)) = (V ∩ (𝑓𝑡)))
82 ssv 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓𝑡) ⊆ V
83 sseqin2 4223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑡) ⊆ V ↔ (V ∩ (𝑓𝑡)) = (𝑓𝑡))
8482, 83mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (V ∩ (𝑓𝑡)) = (𝑓𝑡)
8581, 84eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓𝑡) = ∅ → ( (𝑓𝑡) ∩ (𝑓𝑡)) = (𝑓𝑡))
8685eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑡) = ∅ → (( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴 ↔ (𝑓𝑡) ∈ 𝐴))
8786biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓𝑡) = ∅ → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))
8877, 87pm2.61d2 181 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → ((𝑓𝑡) ∈ 𝐴 → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴))
8939, 88mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → ( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴)
90 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝑡) ∈ V
9190intunsn 4987 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑡) ∪ {(𝑓𝑡)}) = ( (𝑓𝑡) ∩ (𝑓𝑡))
92 f1ofn 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑡1-1-onto𝑧𝑓 Fn suc 𝑡)
93 fnsnfv 6988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 Fn suc 𝑡𝑡 ∈ suc 𝑡) → {(𝑓𝑡)} = (𝑓 “ {𝑡}))
9492, 35, 93sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑡1-1-onto𝑧 → {(𝑓𝑡)} = (𝑓 “ {𝑡}))
9594uneq2d 4168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑡1-1-onto𝑧 → ((𝑓𝑡) ∪ {(𝑓𝑡)}) = ((𝑓𝑡) ∪ (𝑓 “ {𝑡})))
96 df-suc 6390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑡 = (𝑡 ∪ {𝑡})
9796imaeq2i 6076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ suc 𝑡) = (𝑓 “ (𝑡 ∪ {𝑡}))
98 imaundi 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ (𝑡 ∪ {𝑡})) = ((𝑓𝑡) ∪ (𝑓 “ {𝑡}))
9997, 98eqtr2i 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑡) ∪ (𝑓 “ {𝑡})) = (𝑓 “ suc 𝑡)
10095, 99eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑡1-1-onto𝑧 → ((𝑓𝑡) ∪ {(𝑓𝑡)}) = (𝑓 “ suc 𝑡))
101 f1ofo 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑡1-1-onto𝑧𝑓:suc 𝑡onto𝑧)
102 foima 6825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑡onto𝑧 → (𝑓 “ suc 𝑡) = 𝑧)
103101, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑡1-1-onto𝑧 → (𝑓 “ suc 𝑡) = 𝑧)
104100, 103eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑡1-1-onto𝑧 → ((𝑓𝑡) ∪ {(𝑓𝑡)}) = 𝑧)
105104inteqd 4951 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑡1-1-onto𝑧 ((𝑓𝑡) ∪ {(𝑓𝑡)}) = 𝑧)
10691, 105eqtr3id 2791 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:suc 𝑡1-1-onto𝑧 → ( (𝑓𝑡) ∩ (𝑓𝑡)) = 𝑧)
107106eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:suc 𝑡1-1-onto𝑧 → (( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴 𝑧𝐴))
108107ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → (( (𝑓𝑡) ∩ (𝑓𝑡)) ∈ 𝐴 𝑧𝐴))
10989, 108mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧𝐴𝑓:suc 𝑡1-1-onto𝑧) ∧ (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) ∧ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)) → 𝑧𝐴)
110109exp43 436 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐴 → (𝑓:suc 𝑡1-1-onto𝑧 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴))))
111110exlimdv 1933 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐴 → (∃𝑓 𝑓:suc 𝑡1-1-onto𝑧 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴))))
11231, 111biimtrid 242 . . . . . . . . . . . . . . . . . 18 (𝑧𝐴 → (suc 𝑡𝑧 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴))))
113112imp 406 . . . . . . . . . . . . . . . . 17 ((𝑧𝐴 ∧ suc 𝑡𝑧) → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴)))
114113adantlr 715 . . . . . . . . . . . . . . . 16 (((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧) → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴)))
115114com13 88 . . . . . . . . . . . . . . 15 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → (((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧) → 𝑧𝐴)))
11629, 30, 115alrimd 2215 . . . . . . . . . . . . . 14 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧) → 𝑧𝐴)))
117116a1i 11 . . . . . . . . . . . . 13 (𝑡 ∈ ω → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑡𝑧) → 𝑧𝐴) → ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ suc 𝑡𝑧) → 𝑧𝐴))))
1188, 12, 16, 28, 117finds2 7920 . . . . . . . . . . . 12 (𝑤 ∈ ω → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴)))
119 sp 2183 . . . . . . . . . . . 12 (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴) → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴))
120118, 119syl6 35 . . . . . . . . . . 11 (𝑤 ∈ ω → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑤𝑧) → 𝑧𝐴)))
121120exp4a 431 . . . . . . . . . 10 (𝑤 ∈ ω → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ((𝑧𝐴𝑧 ≠ ∅) → (𝑤𝑧 𝑧𝐴))))
122121com24 95 . . . . . . . . 9 (𝑤 ∈ ω → (𝑤𝑧 → ((𝑧𝐴𝑧 ≠ ∅) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴))))
1234, 122sylbird 260 . . . . . . . 8 (𝑤 ∈ ω → (𝑧𝑤 → ((𝑧𝐴𝑧 ≠ ∅) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴))))
124123rexlimiv 3148 . . . . . . 7 (∃𝑤 ∈ ω 𝑧𝑤 → ((𝑧𝐴𝑧 ≠ ∅) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴)))
1251, 124sylbi 217 . . . . . 6 (𝑧 ∈ Fin → ((𝑧𝐴𝑧 ≠ ∅) → (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 𝑧𝐴)))
126125com13 88 . . . . 5 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ((𝑧𝐴𝑧 ≠ ∅) → (𝑧 ∈ Fin → 𝑧𝐴)))
127126impd 410 . . . 4 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
128127alrimiv 1927 . . 3 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 → ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
129 zfpair2 5433 . . . . . 6 {𝑣, 𝑢} ∈ V
130 sseq1 4009 . . . . . . . . 9 (𝑧 = {𝑣, 𝑢} → (𝑧𝐴 ↔ {𝑣, 𝑢} ⊆ 𝐴))
131 neeq1 3003 . . . . . . . . 9 (𝑧 = {𝑣, 𝑢} → (𝑧 ≠ ∅ ↔ {𝑣, 𝑢} ≠ ∅))
132130, 131anbi12d 632 . . . . . . . 8 (𝑧 = {𝑣, 𝑢} → ((𝑧𝐴𝑧 ≠ ∅) ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅)))
133 eleq1 2829 . . . . . . . 8 (𝑧 = {𝑣, 𝑢} → (𝑧 ∈ Fin ↔ {𝑣, 𝑢} ∈ Fin))
134132, 133anbi12d 632 . . . . . . 7 (𝑧 = {𝑣, 𝑢} → (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin)))
135 inteq 4949 . . . . . . . 8 (𝑧 = {𝑣, 𝑢} → 𝑧 = {𝑣, 𝑢})
136135eleq1d 2826 . . . . . . 7 (𝑧 = {𝑣, 𝑢} → ( 𝑧𝐴 {𝑣, 𝑢} ∈ 𝐴))
137134, 136imbi12d 344 . . . . . 6 (𝑧 = {𝑣, 𝑢} → ((((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴) ↔ ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → {𝑣, 𝑢} ∈ 𝐴)))
138129, 137spcv 3605 . . . . 5 (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴) → ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) → {𝑣, 𝑢} ∈ 𝐴))
139 vex 3484 . . . . . . 7 𝑣 ∈ V
140 vex 3484 . . . . . . 7 𝑢 ∈ V
141139, 140prss 4820 . . . . . 6 ((𝑣𝐴𝑢𝐴) ↔ {𝑣, 𝑢} ⊆ 𝐴)
142139prnz 4777 . . . . . . 7 {𝑣, 𝑢} ≠ ∅
143142biantru 529 . . . . . 6 ({𝑣, 𝑢} ⊆ 𝐴 ↔ ({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅))
144 prfi 9363 . . . . . . 7 {𝑣, 𝑢} ∈ Fin
145144biantru 529 . . . . . 6 (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ↔ (({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin))
146141, 143, 1453bitrri 298 . . . . 5 ((({𝑣, 𝑢} ⊆ 𝐴 ∧ {𝑣, 𝑢} ≠ ∅) ∧ {𝑣, 𝑢} ∈ Fin) ↔ (𝑣𝐴𝑢𝐴))
147139, 140intpr 4982 . . . . . 6 {𝑣, 𝑢} = (𝑣𝑢)
148147eleq1i 2832 . . . . 5 ( {𝑣, 𝑢} ∈ 𝐴 ↔ (𝑣𝑢) ∈ 𝐴)
149138, 146, 1483imtr3g 295 . . . 4 (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴) → ((𝑣𝐴𝑢𝐴) → (𝑣𝑢) ∈ 𝐴))
150149ralrimivv 3200 . . 3 (∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴) → ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)
151128, 150impbii 209 . 2 (∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴 ↔ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
152 ineq1 4213 . . . 4 (𝑥 = 𝑣 → (𝑥𝑦) = (𝑣𝑦))
153152eleq1d 2826 . . 3 (𝑥 = 𝑣 → ((𝑥𝑦) ∈ 𝐴 ↔ (𝑣𝑦) ∈ 𝐴))
154 ineq2 4214 . . . 4 (𝑦 = 𝑢 → (𝑣𝑦) = (𝑣𝑢))
155154eleq1d 2826 . . 3 (𝑦 = 𝑢 → ((𝑣𝑦) ∈ 𝐴 ↔ (𝑣𝑢) ∈ 𝐴))
156153, 155cbvral2vw 3241 . 2 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑣𝐴𝑢𝐴 (𝑣𝑢) ∈ 𝐴)
157 df-3an 1089 . . . 4 ((𝑧𝐴𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) ↔ ((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin))
158157imbi1i 349 . . 3 (((𝑧𝐴𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → 𝑧𝐴) ↔ (((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
159158albii 1819 . 2 (∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → 𝑧𝐴) ↔ ∀𝑧(((𝑧𝐴𝑧 ≠ ∅) ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
160151, 156, 1593bitr4i 303 1 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧𝐴𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → 𝑧𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087  wal 1538   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626  {cpr 4628   cint 4946   class class class wbr 5143  ccnv 5684  ran crn 5686  cima 5688  suc csuc 6386  Fun wfun 6555   Fn wfn 6556  wf 6557  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560  cfv 6561  ωcom 7887  cen 8982  Fincfn 8985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-2o 8507  df-en 8986  df-fin 8989
This theorem is referenced by:  dffi2  9463  istop2g  22902  neificl  37760
  Copyright terms: Public domain W3C validator