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

Theorem fiintim 6945
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 6778 . . . . . 6 (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥𝑦)
2 ensym 6798 . . . . . . . 8 (𝑥𝑦𝑦𝑥)
3 breq1 4020 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (𝑦𝑥 ↔ ∅ ≈ 𝑥))
43anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
54imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = ∅ → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
65albidv 1834 . . . . . . . . . . . 12 (𝑦 = ∅ → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
7 breq1 4020 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
87anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥)))
98imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
109albidv 1834 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
11 breq1 4020 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑣 → (𝑦𝑥 ↔ suc 𝑣𝑥))
1211anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥)))
1312imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = suc 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
1413albidv 1834 . . . . . . . . . . . 12 (𝑦 = suc 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
15 ensym 6798 . . . . . . . . . . . . . . . . . . 19 (∅ ≈ 𝑥𝑥 ≈ ∅)
16 en0 6812 . . . . . . . . . . . . . . . . . . 19 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
1715, 16sylib 122 . . . . . . . . . . . . . . . . . 18 (∅ ≈ 𝑥𝑥 = ∅)
1817anim1i 340 . . . . . . . . . . . . . . . . 17 ((∅ ≈ 𝑥𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
1918ancoms 268 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
2019adantll 476 . . . . . . . . . . . . . . 15 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21 df-ne 2360 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22 pm3.24 694 . . . . . . . . . . . . . . . . 17 ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
2322pm2.21i 647 . . . . . . . . . . . . . . . 16 ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → 𝑥𝐴)
2421, 23sylan2b 287 . . . . . . . . . . . . . . 15 ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → 𝑥𝐴)
2520, 24syl 14 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2625ax-gen 1459 . . . . . . . . . . . . 13 𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2726a1i 9 . . . . . . . . . . . 12 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴))
28 nfv 1538 . . . . . . . . . . . . . 14 𝑥(𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
29 nfa1 1551 . . . . . . . . . . . . . 14 𝑥𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)
30 simpl 109 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ≠ ∅) → 𝑥𝐴)
31 bren 6764 . . . . . . . . . . . . . . . . . . 19 (suc 𝑣𝑥 ↔ ∃𝑓 𝑓:suc 𝑣1-1-onto𝑥)
32 ssel 3163 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐴 → ((𝑓𝑣) ∈ 𝑥 → (𝑓𝑣) ∈ 𝐴))
33 f1of 5475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣𝑥)
34 vex 2754 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑣 ∈ V
3534sucid 4431 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑣 ∈ suc 𝑣
36 ffvelcdm 5664 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = ∅ → (𝑓𝑣) = (𝑓 “ ∅))
42 ima0 5001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 “ ∅) = ∅
4341, 42eqtrdi 2237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = ∅ → (𝑓𝑣) = ∅)
44 inteq 3861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑣) = ∅ → (𝑓𝑣) = ∅)
45 int0 3872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ = V
4644, 45eqtrdi 2237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) = ∅ → (𝑓𝑣) = V)
4746ineq1d 3349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (V ∩ (𝑓𝑣)))
48 ssv 3191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓𝑣) ⊆ V
49 sseqin2 3368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) ⊆ V ↔ (V ∩ (𝑓𝑣)) = (𝑓𝑣))
5048, 49mpbi 145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (V ∩ (𝑓𝑣)) = (𝑓𝑣)
5147, 50eqtrdi 2237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (𝑓𝑣))
5251eleq1d 2257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑣) = ∅ → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 ↔ (𝑓𝑣) ∈ 𝐴))
5352biimprd 158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓𝑣) = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5554adantl 277 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
56 f1ofun 5477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → Fun 𝑓)
5756ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58 elelsuc 4423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
5958adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60 f1odm 5479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:suc 𝑣1-1-onto𝑥 → dom 𝑓 = suc 𝑣)
6160eleq2d 2258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓𝑣)))
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓𝑣))
68 ne0i 3443 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓‘∅) ∈ (𝑓𝑣) → (𝑓𝑣) ≠ ∅)
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓𝑣) ≠ ∅)
70 imassrn 4995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓𝑣) ⊆ ran 𝑓
71 dff1o2 5480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:suc 𝑣1-1-onto𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑥))
7271simp3bi 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:suc 𝑣1-1-onto𝑥 → ran 𝑓 = 𝑥)
7370, 72sseqtrid 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ⊆ 𝑥)
74 sstr2 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑣) ⊆ 𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7675anim1d 336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
77 f1of1 5474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣1-1𝑥)
78 vex 2754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑥 ∈ V
79 sssucid 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 ⊆ suc 𝑣
80 f1imaen2g 6810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥𝑣 ≈ (𝑓𝑣))
8476, 83jctird 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
85 vex 2754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑓 ∈ V
8685imaex 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓𝑣) ∈ V
87 sseq1 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥𝐴 ↔ (𝑓𝑣) ⊆ 𝐴))
88 neeq1 2372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥 ≠ ∅ ↔ (𝑓𝑣) ≠ ∅))
8987, 88anbi12d 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → ((𝑥𝐴𝑥 ≠ ∅) ↔ ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
90 breq2 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → (𝑣𝑥𝑣 ≈ (𝑓𝑣)))
9189, 90anbi12d 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) ↔ (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
92 inteq 3861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → 𝑥 = (𝑓𝑣))
9392eleq1d 2257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → ( 𝑥𝐴 (𝑓𝑣) ∈ 𝐴))
9491, 93imbi12d 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑓𝑣) → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ↔ ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴)))
9586, 94spcv 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴))
9684, 95sylan9 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (𝑓𝑣) ∈ 𝐴))
97 ineq1 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑣) → (𝑧𝑤) = ( (𝑓𝑣) ∩ 𝑤))
9897eleq1d 2257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑣) → ((𝑧𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴))
99 ineq2 3344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 = (𝑓𝑣) → ( (𝑓𝑣) ∩ 𝑤) = ( (𝑓𝑣) ∩ (𝑓𝑣)))
10099eleq1d 2257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = (𝑓𝑣) → (( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
10198, 100rspc2v 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4632 . . . . . . . . . . . . . . . . . . . . . . . . 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 5549 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝑣) ∈ V
116115intunsn 3896 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ( (𝑓𝑣) ∩ (𝑓𝑣))
117 f1ofn 5476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥𝑓 Fn suc 𝑣)
118 fnsnfv 5590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 Fn suc 𝑣𝑣 ∈ suc 𝑣) → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
119117, 35, 118sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
120119uneq2d 3303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣})))
121 df-suc 4385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑣 = (𝑣 ∪ {𝑣})
122121imaeq2i 4982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123 imaundi 5055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣}))
124122, 123eqtr2i 2210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125120, 124eqtrdi 2237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = (𝑓 “ suc 𝑣))
126 f1ofo 5482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣onto𝑥)
127 foima 5457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129125, 128eqtrd 2221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
130129inteqd 3863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑣1-1-onto𝑥 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
131116, 130eqtr3id 2235 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:suc 𝑣1-1-onto𝑥 → ( (𝑓𝑣) ∩ (𝑓𝑣)) = 𝑥)
132131eleq1d 2257 . . . . . . . . . . . . . . . . . . . . . . 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 1829 . . . . . . . . . . . . . . . . . . 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 1620 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
143142ex 115 . . . . . . . . . . . 12 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
1446, 10, 14, 27, 143finds2 4614 . . . . . . . . . . 11 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
145 sp 1521 . . . . . . . . . . 11 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴))
146144, 145syl6 33 . . . . . . . . . 10 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
147146exp4a 366 . . . . . . . . 9 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑦𝑥 𝑥𝐴))))
148147com24 87 . . . . . . . 8 (𝑦 ∈ ω → (𝑦𝑥 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
1492, 148syl5 32 . . . . . . 7 (𝑦 ∈ ω → (𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
150149rexlimiv 2600 . . . . . 6 (∃𝑦 ∈ ω 𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
1511, 150sylbi 121 . . . . 5 (𝑥 ∈ Fin → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
152151com13 80 . . . 4 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑥 ∈ Fin → 𝑥𝐴)))
153152impd 254 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
154153alrimiv 1884 . 2 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
155 ineq1 3343 . . . 4 (𝑥 = 𝑧 → (𝑥𝑦) = (𝑧𝑦))
156155eleq1d 2257 . . 3 (𝑥 = 𝑧 → ((𝑥𝑦) ∈ 𝐴 ↔ (𝑧𝑦) ∈ 𝐴))
157 ineq2 3344 . . . 4 (𝑦 = 𝑤 → (𝑧𝑦) = (𝑧𝑤))
158157eleq1d 2257 . . 3 (𝑦 = 𝑤 → ((𝑧𝑦) ∈ 𝐴 ↔ (𝑧𝑤) ∈ 𝐴))
159156, 158cbvral2v 2730 . 2 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
160 df-3an 981 . . . 4 ((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161160imbi1i 238 . . 3 (((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
162161albii 1480 . 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 979  wal 1361   = wceq 1363  wex 1502  wcel 2159  wne 2359  wral 2467  wrex 2468  Vcvv 2751  cun 3141  cin 3142  wss 3143  c0 3436  {csn 3606   cint 3858   class class class wbr 4017  suc csuc 4379  ωcom 4603  ccnv 4639  dom cdm 4640  ran crn 4641  cima 4643  Fun wfun 5224   Fn wfn 5225  wf 5226  1-1wf1 5227  ontowfo 5228  1-1-ontowf1o 5229  cfv 5230  cen 6755  Fincfn 6757
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-sep 4135  ax-nul 4143  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-iinf 4601
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-ral 2472  df-rex 2473  df-v 2753  df-sbc 2977  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-nul 3437  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-br 4018  df-opab 4079  df-id 4307  df-suc 4385  df-iom 4604  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-er 6552  df-en 6758  df-fin 6760
This theorem is referenced by:  istopfin  13883
  Copyright terms: Public domain W3C validator