ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fiintim GIF version

Theorem fiintim 6958
Description: If a class is closed under pairwise intersections, then it is closed under nonempty finite intersections. The converse would appear to require an additional condition, such as 𝑥 and 𝑦 not being equal, or 𝐴 having decidable equality.

This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.)

Assertion
Ref Expression
fiintim (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 → ∀𝑥((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem fiintim
Dummy variables 𝑧 𝑤 𝑣 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6788 . . . . . 6 (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥𝑦)
2 ensym 6808 . . . . . . . 8 (𝑥𝑦𝑦𝑥)
3 breq1 4021 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (𝑦𝑥 ↔ ∅ ≈ 𝑥))
43anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
54imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = ∅ → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
65albidv 1835 . . . . . . . . . . . 12 (𝑦 = ∅ → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
7 breq1 4021 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
87anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥)))
98imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
109albidv 1835 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
11 breq1 4021 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑣 → (𝑦𝑥 ↔ suc 𝑣𝑥))
1211anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥)))
1312imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = suc 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
1413albidv 1835 . . . . . . . . . . . 12 (𝑦 = suc 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
15 ensym 6808 . . . . . . . . . . . . . . . . . . 19 (∅ ≈ 𝑥𝑥 ≈ ∅)
16 en0 6822 . . . . . . . . . . . . . . . . . . 19 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
1715, 16sylib 122 . . . . . . . . . . . . . . . . . 18 (∅ ≈ 𝑥𝑥 = ∅)
1817anim1i 340 . . . . . . . . . . . . . . . . 17 ((∅ ≈ 𝑥𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
1918ancoms 268 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
2019adantll 476 . . . . . . . . . . . . . . 15 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21 df-ne 2361 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22 pm3.24 694 . . . . . . . . . . . . . . . . 17 ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
2322pm2.21i 647 . . . . . . . . . . . . . . . 16 ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → 𝑥𝐴)
2421, 23sylan2b 287 . . . . . . . . . . . . . . 15 ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → 𝑥𝐴)
2520, 24syl 14 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2625ax-gen 1460 . . . . . . . . . . . . 13 𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2726a1i 9 . . . . . . . . . . . 12 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴))
28 nfv 1539 . . . . . . . . . . . . . 14 𝑥(𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
29 nfa1 1552 . . . . . . . . . . . . . 14 𝑥𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)
30 simpl 109 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ≠ ∅) → 𝑥𝐴)
31 bren 6774 . . . . . . . . . . . . . . . . . . 19 (suc 𝑣𝑥 ↔ ∃𝑓 𝑓:suc 𝑣1-1-onto𝑥)
32 ssel 3164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐴 → ((𝑓𝑣) ∈ 𝑥 → (𝑓𝑣) ∈ 𝐴))
33 f1of 5480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣𝑥)
34 vex 2755 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑣 ∈ V
3534sucid 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑣 ∈ suc 𝑣
36 ffvelcdm 5670 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:suc 𝑣𝑥𝑣 ∈ suc 𝑣) → (𝑓𝑣) ∈ 𝑥)
3733, 35, 36sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ∈ 𝑥)
3832, 37impel 280 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) → (𝑓𝑣) ∈ 𝐴)
3938adantr 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑓𝑣) ∈ 𝐴)
4039adantlll 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑓𝑣) ∈ 𝐴)
41 imaeq2 4984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = ∅ → (𝑓𝑣) = (𝑓 “ ∅))
42 ima0 5005 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 “ ∅) = ∅
4341, 42eqtrdi 2238 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = ∅ → (𝑓𝑣) = ∅)
44 inteq 3862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑣) = ∅ → (𝑓𝑣) = ∅)
45 int0 3873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ = V
4644, 45eqtrdi 2238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) = ∅ → (𝑓𝑣) = V)
4746ineq1d 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (V ∩ (𝑓𝑣)))
48 ssv 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓𝑣) ⊆ V
49 sseqin2 3369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) ⊆ V ↔ (V ∩ (𝑓𝑣)) = (𝑓𝑣))
5048, 49mpbi 145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (V ∩ (𝑓𝑣)) = (𝑓𝑣)
5147, 50eqtrdi 2238 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (𝑓𝑣))
5251eleq1d 2258 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑣) = ∅ → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 ↔ (𝑓𝑣) ∈ 𝐴))
5352biimprd 158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓𝑣) = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5554adantl 277 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
56 f1ofun 5482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → Fun 𝑓)
5756ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58 elelsuc 4427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
5958adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60 f1odm 5484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:suc 𝑣1-1-onto𝑥 → dom 𝑓 = suc 𝑣)
6160eleq2d 2259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥 → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
6261ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
6359, 62mpbird 167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓)
6457, 63jca 306 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓))
65 simpr 110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣)
66 funfvima 5769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓𝑣)))
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓𝑣))
68 ne0i 3444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓‘∅) ∈ (𝑓𝑣) → (𝑓𝑣) ≠ ∅)
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓𝑣) ≠ ∅)
70 imassrn 4999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓𝑣) ⊆ ran 𝑓
71 dff1o2 5485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:suc 𝑣1-1-onto𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑥))
7271simp3bi 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:suc 𝑣1-1-onto𝑥 → ran 𝑓 = 𝑥)
7370, 72sseqtrid 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ⊆ 𝑥)
74 sstr2 3177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑣) ⊆ 𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7675anim1d 336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
77 f1of1 5479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣1-1𝑥)
78 vex 2755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑥 ∈ V
79 sssucid 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 ⊆ suc 𝑣
80 f1imaen2g 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:suc 𝑣1-1𝑥𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣𝑣 ∈ V)) → (𝑓𝑣) ≈ 𝑣)
8179, 34, 80mpanr12 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:suc 𝑣1-1𝑥𝑥 ∈ V) → (𝑓𝑣) ≈ 𝑣)
8277, 78, 81sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ≈ 𝑣)
8382ensymd 6810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥𝑣 ≈ (𝑓𝑣))
8476, 83jctird 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
85 vex 2755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑓 ∈ V
8685imaex 5001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓𝑣) ∈ V
87 sseq1 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥𝐴 ↔ (𝑓𝑣) ⊆ 𝐴))
88 neeq1 2373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥 ≠ ∅ ↔ (𝑓𝑣) ≠ ∅))
8987, 88anbi12d 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → ((𝑥𝐴𝑥 ≠ ∅) ↔ ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
90 breq2 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → (𝑣𝑥𝑣 ≈ (𝑓𝑣)))
9189, 90anbi12d 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) ↔ (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
92 inteq 3862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → 𝑥 = (𝑓𝑣))
9392eleq1d 2258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → ( 𝑥𝐴 (𝑓𝑣) ∈ 𝐴))
9491, 93imbi12d 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑓𝑣) → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ↔ ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴)))
9586, 94spcv 2846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴))
9684, 95sylan9 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (𝑓𝑣) ∈ 𝐴))
97 ineq1 3344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑣) → (𝑧𝑤) = ( (𝑓𝑣) ∩ 𝑤))
9897eleq1d 2258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑣) → ((𝑧𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴))
99 ineq2 3345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 = (𝑓𝑣) → ( (𝑓𝑣) ∩ 𝑤) = ( (𝑓𝑣) ∩ (𝑓𝑣)))
10099eleq1d 2258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = (𝑓𝑣) → (( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
10198, 100rspc2v 2869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( (𝑓𝑣) ∈ 𝐴 ∧ (𝑓𝑣) ∈ 𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
102101ex 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑣) ∈ 𝐴 → ((𝑓𝑣) ∈ 𝐴 → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
10396, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ∈ 𝐴 → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))
104103com4r 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))
105104exp5c 376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (𝑥𝐴 → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))))
106105com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐴 → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))))
107106imp43 355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
108107adantlll 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
109108adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
11069, 109mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
111 0elnn 4636 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112111ad3antrrr 492 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
11355, 110, 112mpjaodan 799 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
11440, 113mpd 13 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)
11585, 34fvex 5554 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝑣) ∈ V
116115intunsn 3897 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ( (𝑓𝑣) ∩ (𝑓𝑣))
117 f1ofn 5481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥𝑓 Fn suc 𝑣)
118 fnsnfv 5596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 Fn suc 𝑣𝑣 ∈ suc 𝑣) → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
119117, 35, 118sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
120119uneq2d 3304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣})))
121 df-suc 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑣 = (𝑣 ∪ {𝑣})
122121imaeq2i 4986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123 imaundi 5059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣}))
124122, 123eqtr2i 2211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125120, 124eqtrdi 2238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = (𝑓 “ suc 𝑣))
126 f1ofo 5487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣onto𝑥)
127 foima 5462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129125, 128eqtrd 2222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
130129inteqd 3864 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑣1-1-onto𝑥 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
131116, 130eqtr3id 2236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:suc 𝑣1-1-onto𝑥 → ( (𝑓𝑣) ∩ (𝑓𝑣)) = 𝑥)
132131eleq1d 2258 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:suc 𝑣1-1-onto𝑥 → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 𝑥𝐴))
133132ad2antlr 489 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 𝑥𝐴))
134114, 133mpbid 147 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → 𝑥𝐴)
135134exp43 372 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
136135exlimdv 1830 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (∃𝑓 𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
13731, 136biimtrid 152 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (suc 𝑣𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
138137expimpd 363 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → ((𝑥𝐴 ∧ suc 𝑣𝑥) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
13930, 138sylani 406 . . . . . . . . . . . . . . . 16 (𝑣 ∈ ω → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
140139com24 87 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
141140imp 124 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
14228, 29, 141alrimd 1621 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
143142ex 115 . . . . . . . . . . . 12 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
1446, 10, 14, 27, 143finds2 4618 . . . . . . . . . . 11 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
145 sp 1522 . . . . . . . . . . 11 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴))
146144, 145syl6 33 . . . . . . . . . 10 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
147146exp4a 366 . . . . . . . . 9 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑦𝑥 𝑥𝐴))))
148147com24 87 . . . . . . . 8 (𝑦 ∈ ω → (𝑦𝑥 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
1492, 148syl5 32 . . . . . . 7 (𝑦 ∈ ω → (𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
150149rexlimiv 2601 . . . . . 6 (∃𝑦 ∈ ω 𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
1511, 150sylbi 121 . . . . 5 (𝑥 ∈ Fin → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
152151com13 80 . . . 4 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑥 ∈ Fin → 𝑥𝐴)))
153152impd 254 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
154153alrimiv 1885 . 2 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
155 ineq1 3344 . . . 4 (𝑥 = 𝑧 → (𝑥𝑦) = (𝑧𝑦))
156155eleq1d 2258 . . 3 (𝑥 = 𝑧 → ((𝑥𝑦) ∈ 𝐴 ↔ (𝑧𝑦) ∈ 𝐴))
157 ineq2 3345 . . . 4 (𝑦 = 𝑤 → (𝑧𝑦) = (𝑧𝑤))
158157eleq1d 2258 . . 3 (𝑦 = 𝑤 → ((𝑧𝑦) ∈ 𝐴 ↔ (𝑧𝑤) ∈ 𝐴))
159156, 158cbvral2v 2731 . 2 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
160 df-3an 982 . . . 4 ((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161160imbi1i 238 . . 3 (((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
162161albii 1481 . 2 (∀𝑥((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
163154, 159, 1623imtr4i 201 1 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 → ∀𝑥((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  w3a 980  wal 1362   = wceq 1364  wex 1503  wcel 2160  wne 2360  wral 2468  wrex 2469  Vcvv 2752  cun 3142  cin 3143  wss 3144  c0 3437  {csn 3607   cint 3859   class class class wbr 4018  suc csuc 4383  ωcom 4607  ccnv 4643  dom cdm 4644  ran crn 4645  cima 4647  Fun wfun 5229   Fn wfn 5230  wf 5231  1-1wf1 5232  ontowfo 5233  1-1-ontowf1o 5234  cfv 5235  cen 6765  Fincfn 6767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-iinf 4605
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-id 4311  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-er 6560  df-en 6768  df-fin 6770
This theorem is referenced by:  istopfin  13977
  Copyright terms: Public domain W3C validator