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

Theorem fiintim 6862
 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 6695 . . . . . 6 (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥𝑦)
2 ensym 6715 . . . . . . . 8 (𝑥𝑦𝑦𝑥)
3 breq1 3964 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (𝑦𝑥 ↔ ∅ ≈ 𝑥))
43anbi2d 460 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
54imbi1d 230 . . . . . . . . . . . . 13 (𝑦 = ∅ → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
65albidv 1801 . . . . . . . . . . . 12 (𝑦 = ∅ → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
7 breq1 3964 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
87anbi2d 460 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥)))
98imbi1d 230 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
109albidv 1801 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
11 breq1 3964 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑣 → (𝑦𝑥 ↔ suc 𝑣𝑥))
1211anbi2d 460 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥)))
1312imbi1d 230 . . . . . . . . . . . . 13 (𝑦 = suc 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
1413albidv 1801 . . . . . . . . . . . 12 (𝑦 = suc 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
15 ensym 6715 . . . . . . . . . . . . . . . . . . 19 (∅ ≈ 𝑥𝑥 ≈ ∅)
16 en0 6729 . . . . . . . . . . . . . . . . . . 19 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
1715, 16sylib 121 . . . . . . . . . . . . . . . . . 18 (∅ ≈ 𝑥𝑥 = ∅)
1817anim1i 338 . . . . . . . . . . . . . . . . 17 ((∅ ≈ 𝑥𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
1918ancoms 266 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
2019adantll 468 . . . . . . . . . . . . . . 15 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21 df-ne 2325 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22 pm3.24 683 . . . . . . . . . . . . . . . . 17 ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
2322pm2.21i 636 . . . . . . . . . . . . . . . 16 ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → 𝑥𝐴)
2421, 23sylan2b 285 . . . . . . . . . . . . . . 15 ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → 𝑥𝐴)
2520, 24syl 14 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2625ax-gen 1426 . . . . . . . . . . . . 13 𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2726a1i 9 . . . . . . . . . . . 12 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴))
28 nfv 1505 . . . . . . . . . . . . . 14 𝑥(𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
29 nfa1 1518 . . . . . . . . . . . . . 14 𝑥𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)
30 simpl 108 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ≠ ∅) → 𝑥𝐴)
31 bren 6681 . . . . . . . . . . . . . . . . . . 19 (suc 𝑣𝑥 ↔ ∃𝑓 𝑓:suc 𝑣1-1-onto𝑥)
32 ssel 3118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐴 → ((𝑓𝑣) ∈ 𝑥 → (𝑓𝑣) ∈ 𝐴))
33 f1of 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣𝑥)
34 vex 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑣 ∈ V
3534sucid 4372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑣 ∈ suc 𝑣
36 ffvelrn 5593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:suc 𝑣𝑥𝑣 ∈ suc 𝑣) → (𝑓𝑣) ∈ 𝑥)
3733, 35, 36sylancl 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ∈ 𝑥)
3832, 37impel 278 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) → (𝑓𝑣) ∈ 𝐴)
3938adantr 274 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑓𝑣) ∈ 𝐴)
4039adantlll 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑓𝑣) ∈ 𝐴)
41 imaeq2 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = ∅ → (𝑓𝑣) = (𝑓 “ ∅))
42 ima0 4938 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 “ ∅) = ∅
4341, 42eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = ∅ → (𝑓𝑣) = ∅)
44 inteq 3806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑣) = ∅ → (𝑓𝑣) = ∅)
45 int0 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ = V
4644, 45eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) = ∅ → (𝑓𝑣) = V)
4746ineq1d 3303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (V ∩ (𝑓𝑣)))
48 ssv 3146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓𝑣) ⊆ V
49 sseqin2 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) ⊆ V ↔ (V ∩ (𝑓𝑣)) = (𝑓𝑣))
5048, 49mpbi 144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (V ∩ (𝑓𝑣)) = (𝑓𝑣)
5147, 50eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (𝑓𝑣))
5251eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑣) = ∅ → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 ↔ (𝑓𝑣) ∈ 𝐴))
5352biimprd 157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓𝑣) = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5554adantl 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
56 f1ofun 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → Fun 𝑓)
5756ad3antlr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58 elelsuc 4364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
5958adantl 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60 f1odm 5411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:suc 𝑣1-1-onto𝑥 → dom 𝑓 = suc 𝑣)
6160eleq2d 2224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥 → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
6261ad3antlr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (∅ ∈ dom 𝑓 ↔ ∅ ∈ suc 𝑣))
6359, 62mpbird 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ dom 𝑓)
6457, 63jca 304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (Fun 𝑓 ∧ ∅ ∈ dom 𝑓))
65 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ 𝑣)
66 funfvima 5689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓𝑣)))
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓𝑣))
68 ne0i 3396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓‘∅) ∈ (𝑓𝑣) → (𝑓𝑣) ≠ ∅)
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓𝑣) ≠ ∅)
70 imassrn 4932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓𝑣) ⊆ ran 𝑓
71 dff1o2 5412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:suc 𝑣1-1-onto𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑥))
7271simp3bi 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:suc 𝑣1-1-onto𝑥 → ran 𝑓 = 𝑥)
7370, 72sseqtrid 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ⊆ 𝑥)
74 sstr2 3131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑣) ⊆ 𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7675anim1d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
77 f1of1 5406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣1-1𝑥)
78 vex 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑥 ∈ V
79 sssucid 4370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 ⊆ suc 𝑣
80 f1imaen2g 6727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:suc 𝑣1-1𝑥𝑥 ∈ V) ∧ (𝑣 ⊆ suc 𝑣𝑣 ∈ V)) → (𝑓𝑣) ≈ 𝑣)
8179, 34, 80mpanr12 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:suc 𝑣1-1𝑥𝑥 ∈ V) → (𝑓𝑣) ≈ 𝑣)
8277, 78, 81sylancl 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ≈ 𝑣)
8382ensymd 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥𝑣 ≈ (𝑓𝑣))
8476, 83jctird 315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
85 vex 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑓 ∈ V
8685imaex 4934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓𝑣) ∈ V
87 sseq1 3147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥𝐴 ↔ (𝑓𝑣) ⊆ 𝐴))
88 neeq1 2337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥 ≠ ∅ ↔ (𝑓𝑣) ≠ ∅))
8987, 88anbi12d 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → ((𝑥𝐴𝑥 ≠ ∅) ↔ ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
90 breq2 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → (𝑣𝑥𝑣 ≈ (𝑓𝑣)))
9189, 90anbi12d 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) ↔ (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
92 inteq 3806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → 𝑥 = (𝑓𝑣))
9392eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → ( 𝑥𝐴 (𝑓𝑣) ∈ 𝐴))
9491, 93imbi12d 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑓𝑣) → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ↔ ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴)))
9586, 94spcv 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴))
9684, 95sylan9 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (𝑓𝑣) ∈ 𝐴))
97 ineq1 3297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑣) → (𝑧𝑤) = ( (𝑓𝑣) ∩ 𝑤))
9897eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑣) → ((𝑧𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴))
99 ineq2 3298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 = (𝑓𝑣) → ( (𝑓𝑣) ∩ 𝑤) = ( (𝑓𝑣) ∩ (𝑓𝑣)))
10099eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = (𝑓𝑣) → (( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
10198, 100rspc2v 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( (𝑓𝑣) ∈ 𝐴 ∧ (𝑓𝑣) ∈ 𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
102101ex 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ( (𝑓𝑣) ∈ 𝐴 → ((𝑓𝑣) ∈ 𝐴 → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
10396, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ∈ 𝐴 → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))
104103com4r 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))
105104exp5c 374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (𝑥𝐴 → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))))
106105com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐴 → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))))))
107106imp43 353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥𝐴𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
108107adantlll 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
109108adantr 274 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓𝑣) ≠ ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)))
11069, 109mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
111 0elnn 4572 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112111ad3antrrr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
11355, 110, 112mpjaodan 788 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
11440, 113mpd 13 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)
11585, 34fvex 5481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝑣) ∈ V
116115intunsn 3841 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ( (𝑓𝑣) ∩ (𝑓𝑣))
117 f1ofn 5408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥𝑓 Fn suc 𝑣)
118 fnsnfv 5520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 Fn suc 𝑣𝑣 ∈ suc 𝑣) → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
119117, 35, 118sylancl 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
120119uneq2d 3257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣})))
121 df-suc 4326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑣 = (𝑣 ∪ {𝑣})
122121imaeq2i 4919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123 imaundi 4991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣}))
124122, 123eqtr2i 2176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125120, 124eqtrdi 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = (𝑓 “ suc 𝑣))
126 f1ofo 5414 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣onto𝑥)
127 foima 5390 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129125, 128eqtrd 2187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
130129inteqd 3808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑣1-1-onto𝑥 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
131116, 130syl5eqr 2201 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:suc 𝑣1-1-onto𝑥 → ( (𝑓𝑣) ∩ (𝑓𝑣)) = 𝑥)
132131eleq1d 2223 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:suc 𝑣1-1-onto𝑥 → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 𝑥𝐴))
133132ad2antlr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 𝑥𝐴))
134114, 133mpbid 146 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → 𝑥𝐴)
135134exp43 370 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
136135exlimdv 1796 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (∃𝑓 𝑓:suc 𝑣1-1-onto𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
13731, 136syl5bi 151 . . . . . . . . . . . . . . . . . 18 ((𝑣 ∈ ω ∧ 𝑥𝐴) → (suc 𝑣𝑥 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
138137expimpd 361 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ω → ((𝑥𝐴 ∧ suc 𝑣𝑥) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
13930, 138sylani 404 . . . . . . . . . . . . . . . 16 (𝑣 ∈ ω → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
140139com24 87 . . . . . . . . . . . . . . 15 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
141140imp 123 . . . . . . . . . . . . . 14 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
14228, 29, 141alrimd 1587 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
143142ex 114 . . . . . . . . . . . 12 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
1446, 10, 14, 27, 143finds2 4554 . . . . . . . . . . 11 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
145 sp 1488 . . . . . . . . . . 11 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴))
146144, 145syl6 33 . . . . . . . . . 10 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
147146exp4a 364 . . . . . . . . 9 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑦𝑥 𝑥𝐴))))
148147com24 87 . . . . . . . 8 (𝑦 ∈ ω → (𝑦𝑥 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
1492, 148syl5 32 . . . . . . 7 (𝑦 ∈ ω → (𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
150149rexlimiv 2565 . . . . . 6 (∃𝑦 ∈ ω 𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
1511, 150sylbi 120 . . . . 5 (𝑥 ∈ Fin → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
152151com13 80 . . . 4 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑥 ∈ Fin → 𝑥𝐴)))
153152impd 252 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
154153alrimiv 1851 . 2 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
155 ineq1 3297 . . . 4 (𝑥 = 𝑧 → (𝑥𝑦) = (𝑧𝑦))
156155eleq1d 2223 . . 3 (𝑥 = 𝑧 → ((𝑥𝑦) ∈ 𝐴 ↔ (𝑧𝑦) ∈ 𝐴))
157 ineq2 3298 . . . 4 (𝑦 = 𝑤 → (𝑧𝑦) = (𝑧𝑤))
158157eleq1d 2223 . . 3 (𝑦 = 𝑤 → ((𝑧𝑦) ∈ 𝐴 ↔ (𝑧𝑤) ∈ 𝐴))
159156, 158cbvral2v 2688 . 2 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
160 df-3an 965 . . . 4 ((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161160imbi1i 237 . . 3 (((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
162161albii 1447 . 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 698   ∧ w3a 963  ∀wal 1330   = wceq 1332  ∃wex 1469   ∈ wcel 2125   ≠ wne 2324  ∀wral 2432  ∃wrex 2433  Vcvv 2709   ∪ cun 3096   ∩ cin 3097   ⊆ wss 3098  ∅c0 3390  {csn 3556  ∩ cint 3803   class class class wbr 3961  suc csuc 4320  ωcom 4543  ◡ccnv 4578  dom cdm 4579  ran crn 4580   “ cima 4582  Fun wfun 5157   Fn wfn 5158  ⟶wf 5159  –1-1→wf1 5160  –onto→wfo 5161  –1-1-onto→wf1o 5162  ‘cfv 5163   ≈ cen 6672  Fincfn 6674 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-iinf 4541 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-ral 2437  df-rex 2438  df-v 2711  df-sbc 2934  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-br 3962  df-opab 4022  df-id 4248  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-er 6469  df-en 6675  df-fin 6677 This theorem is referenced by:  istopfin  12337
 Copyright terms: Public domain W3C validator