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

Theorem fiintim 6693
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 6532 . . . . . 6 (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥𝑦)
2 ensym 6552 . . . . . . . 8 (𝑥𝑦𝑦𝑥)
3 breq1 3854 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (𝑦𝑥 ↔ ∅ ≈ 𝑥))
43anbi2d 453 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
54imbi1d 230 . . . . . . . . . . . . 13 (𝑦 = ∅ → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
65albidv 1753 . . . . . . . . . . . 12 (𝑦 = ∅ → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
7 breq1 3854 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
87anbi2d 453 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥)))
98imbi1d 230 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
109albidv 1753 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
11 breq1 3854 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑣 → (𝑦𝑥 ↔ suc 𝑣𝑥))
1211anbi2d 453 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥)))
1312imbi1d 230 . . . . . . . . . . . . 13 (𝑦 = suc 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
1413albidv 1753 . . . . . . . . . . . 12 (𝑦 = suc 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
15 ensym 6552 . . . . . . . . . . . . . . . . . . 19 (∅ ≈ 𝑥𝑥 ≈ ∅)
16 en0 6566 . . . . . . . . . . . . . . . . . . 19 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
1715, 16sylib 121 . . . . . . . . . . . . . . . . . 18 (∅ ≈ 𝑥𝑥 = ∅)
1817anim1i 334 . . . . . . . . . . . . . . . . 17 ((∅ ≈ 𝑥𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
1918ancoms 265 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
2019adantll 461 . . . . . . . . . . . . . . 15 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21 df-ne 2257 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22 pm3.24 663 . . . . . . . . . . . . . . . . 17 ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
2322pm2.21i 611 . . . . . . . . . . . . . . . 16 ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → 𝑥𝐴)
2421, 23sylan2b 282 . . . . . . . . . . . . . . 15 ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → 𝑥𝐴)
2520, 24syl 14 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2625ax-gen 1384 . . . . . . . . . . . . 13 𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2726a1i 9 . . . . . . . . . . . 12 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴))
28 nfv 1467 . . . . . . . . . . . . . 14 𝑥(𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
29 nfa1 1480 . . . . . . . . . . . . . 14 𝑥𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)
30 simpl 108 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ≠ ∅) → 𝑥𝐴)
31 bren 6518 . . . . . . . . . . . . . . . . . . 19 (suc 𝑣𝑥 ↔ ∃𝑓 𝑓:suc 𝑣1-1-onto𝑥)
32 ssel 3020 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐴 → ((𝑓𝑣) ∈ 𝑥 → (𝑓𝑣) ∈ 𝐴))
33 f1of 5266 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣𝑥)
34 vex 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑣 ∈ V
3534sucid 4253 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑣 ∈ suc 𝑣
36 ffvelrn 5446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:suc 𝑣𝑥𝑣 ∈ suc 𝑣) → (𝑓𝑣) ∈ 𝑥)
3733, 35, 36sylancl 405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ∈ 𝑥)
3832, 37impel 275 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) → (𝑓𝑣) ∈ 𝐴)
3938adantr 271 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑓𝑣) ∈ 𝐴)
4039adantlll 465 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑓𝑣) ∈ 𝐴)
41 imaeq2 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = ∅ → (𝑓𝑣) = (𝑓 “ ∅))
42 ima0 4804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 “ ∅) = ∅
4341, 42syl6eq 2137 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = ∅ → (𝑓𝑣) = ∅)
44 inteq 3697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑣) = ∅ → (𝑓𝑣) = ∅)
45 int0 3708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ = V
4644, 45syl6eq 2137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) = ∅ → (𝑓𝑣) = V)
4746ineq1d 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (V ∩ (𝑓𝑣)))
48 ssv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓𝑣) ⊆ V
49 sseqin2 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) ⊆ V ↔ (V ∩ (𝑓𝑣)) = (𝑓𝑣))
5048, 49mpbi 144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (V ∩ (𝑓𝑣)) = (𝑓𝑣)
5147, 50syl6eq 2137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (𝑓𝑣))
5251eleq1d 2157 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑣) = ∅ → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 ↔ (𝑓𝑣) ∈ 𝐴))
5352biimprd 157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓𝑣) = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5554adantl 272 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
56 f1ofun 5268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → Fun 𝑓)
5756ad3antlr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58 elelsuc 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
5958adantl 272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60 f1odm 5270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:suc 𝑣1-1-onto𝑥 → dom 𝑓 = suc 𝑣)
6160eleq2d 2158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥 → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
6261ad3antlr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
6359, 62mpbird 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓)
6457, 63jca 301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓))
65 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣)
66 funfvima 5540 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓𝑣)))
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓𝑣))
68 ne0i 3293 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓‘∅) ∈ (𝑓𝑣) → (𝑓𝑣) ≠ ∅)
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓𝑣) ≠ ∅)
70 imassrn 4798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓𝑣) ⊆ ran 𝑓
71 dff1o2 5271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:suc 𝑣1-1-onto𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑥))
7271simp3bi 961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:suc 𝑣1-1-onto𝑥 → ran 𝑓 = 𝑥)
7370, 72syl5sseq 3075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ⊆ 𝑥)
74 sstr2 3033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑣) ⊆ 𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7675anim1d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
77 f1of1 5265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣1-1𝑥)
78 vex 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑥 ∈ V
79 sssucid 4251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 ⊆ suc 𝑣
80 f1imaen2g 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:suc 𝑣1-1𝑥𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣𝑣 ∈ V)) → (𝑓𝑣) ≈ 𝑣)
8179, 34, 80mpanr12 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:suc 𝑣1-1𝑥𝑥 ∈ V) → (𝑓𝑣) ≈ 𝑣)
8277, 78, 81sylancl 405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ≈ 𝑣)
8382ensymd 6554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥𝑣 ≈ (𝑓𝑣))
8476, 83jctird 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
85 vex 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑓 ∈ V
8685imaex 4800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓𝑣) ∈ V
87 sseq1 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥𝐴 ↔ (𝑓𝑣) ⊆ 𝐴))
88 neeq1 2269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥 ≠ ∅ ↔ (𝑓𝑣) ≠ ∅))
8987, 88anbi12d 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → ((𝑥𝐴𝑥 ≠ ∅) ↔ ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
90 breq2 3855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → (𝑣𝑥𝑣 ≈ (𝑓𝑣)))
9189, 90anbi12d 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) ↔ (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
92 inteq 3697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → 𝑥 = (𝑓𝑣))
9392eleq1d 2157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → ( 𝑥𝐴 (𝑓𝑣) ∈ 𝐴))
9491, 93imbi12d 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑓𝑣) → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ↔ ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴)))
9586, 94spcv 2713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴))
9684, 95sylan9 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (𝑓𝑣) ∈ 𝐴))
97 ineq1 3195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑣) → (𝑧𝑤) = ( (𝑓𝑣) ∩ 𝑤))
9897eleq1d 2157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑣) → ((𝑧𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴))
99 ineq2 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 = (𝑓𝑣) → ( (𝑓𝑣) ∩ 𝑤) = ( (𝑓𝑣) ∩ (𝑓𝑣)))
10099eleq1d 2157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = (𝑓𝑣) → (( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
10198, 100rspc2v 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( (𝑓𝑣) ∈ 𝐴 ∧ (𝑓𝑣) ∈ 𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
102101ex 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑣) ∈ 𝐴 → ((𝑓𝑣) ∈ 𝐴 → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
10396, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ∈ 𝐴 → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))
104103com4r 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))
105104exp5c 369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (𝑥𝐴 → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))))
106105com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐴 → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))))
107106imp43 348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
108107adantlll 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
109108adantr 271 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
11069, 109mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
111 0elnn 4445 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112111ad3antrrr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
11355, 110, 112mpjaodan 748 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
11440, 113mpd 13 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)
11585, 34fvex 5338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝑣) ∈ V
116115intunsn 3732 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ( (𝑓𝑣) ∩ (𝑓𝑣))
117 f1ofn 5267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥𝑓 Fn suc 𝑣)
118 fnsnfv 5376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 Fn suc 𝑣𝑣 ∈ suc 𝑣) → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
119117, 35, 118sylancl 405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
120119uneq2d 3155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣})))
121 df-suc 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑣 = (𝑣 ∪ {𝑣})
122121imaeq2i 4785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123 imaundi 4857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣}))
124122, 123eqtr2i 2110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125120, 124syl6eq 2137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = (𝑓 “ suc 𝑣))
126 f1ofo 5273 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣onto𝑥)
127 foima 5251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129125, 128eqtrd 2121 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
130129inteqd 3699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑣1-1-onto𝑥 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
131116, 130syl5eqr 2135 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:suc 𝑣1-1-onto𝑥 → ( (𝑓𝑣) ∩ (𝑓𝑣)) = 𝑥)
132131eleq1d 2157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:suc 𝑣1-1-onto𝑥 → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 𝑥𝐴))
133132ad2antlr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 𝑥𝐴))
134114, 133mpbid 146 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → 𝑥𝐴)
135134exp43 365 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
136135exlimdv 1748 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (∃𝑓 𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
13731, 136syl5bi 151 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (suc 𝑣𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
138137expimpd 356 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → ((𝑥𝐴 ∧ suc 𝑣𝑥) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
13930, 138sylani 399 . . . . . . . . . . . . . . . 16 (𝑣 ∈ ω → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
140139com24 87 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
141140imp 123 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
14228, 29, 141alrimd 1547 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
143142ex 114 . . . . . . . . . . . 12 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
1446, 10, 14, 27, 143finds2 4429 . . . . . . . . . . 11 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
145 sp 1447 . . . . . . . . . . 11 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴))
146144, 145syl6 33 . . . . . . . . . 10 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
147146exp4a 359 . . . . . . . . 9 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑦𝑥 𝑥𝐴))))
148147com24 87 . . . . . . . 8 (𝑦 ∈ ω → (𝑦𝑥 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
1492, 148syl5 32 . . . . . . 7 (𝑦 ∈ ω → (𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
150149rexlimiv 2484 . . . . . 6 (∃𝑦 ∈ ω 𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
1511, 150sylbi 120 . . . . 5 (𝑥 ∈ Fin → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
152151com13 80 . . . 4 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑥 ∈ Fin → 𝑥𝐴)))
153152impd 252 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
154153alrimiv 1803 . 2 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
155 ineq1 3195 . . . 4 (𝑥 = 𝑧 → (𝑥𝑦) = (𝑧𝑦))
156155eleq1d 2157 . . 3 (𝑥 = 𝑧 → ((𝑥𝑦) ∈ 𝐴 ↔ (𝑧𝑦) ∈ 𝐴))
157 ineq2 3196 . . . 4 (𝑦 = 𝑤 → (𝑧𝑦) = (𝑧𝑤))
158157eleq1d 2157 . . 3 (𝑦 = 𝑤 → ((𝑧𝑦) ∈ 𝐴 ↔ (𝑧𝑤) ∈ 𝐴))
159156, 158cbvral2v 2599 . 2 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
160 df-3an 927 . . . 4 ((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161160imbi1i 237 . . 3 (((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
162161albii 1405 . 2 (∀𝑥((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
163154, 159, 1623imtr4i 200 1 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 → ∀𝑥((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 665  w3a 925  wal 1288   = wceq 1290  wex 1427  wcel 1439  wne 2256  wral 2360  wrex 2361  Vcvv 2620  cun 2998  cin 2999  wss 3000  c0 3287  {csn 3450   cint 3694   class class class wbr 3851  suc csuc 4201  ωcom 4418  ccnv 4451  dom cdm 4452  ran crn 4453  cima 4455  Fun wfun 5022   Fn wfn 5023  wf 5024  1-1wf1 5025  ontowfo 5026  1-1-ontowf1o 5027  cfv 5028  cen 6509  Fincfn 6511
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-nul 3971  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-iinf 4416
This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-v 2622  df-sbc 2842  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-br 3852  df-opab 3906  df-id 4129  df-suc 4207  df-iom 4419  df-xp 4458  df-rel 4459  df-cnv 4460  df-co 4461  df-dm 4462  df-rn 4463  df-res 4464  df-ima 4465  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-er 6306  df-en 6512  df-fin 6514
This theorem is referenced by:  istopfin  11760
  Copyright terms: Public domain W3C validator