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

Theorem fiintim 6931
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 6764 . . . . . 6 (𝑥 ∈ Fin ↔ ∃𝑦 ∈ ω 𝑥𝑦)
2 ensym 6784 . . . . . . . 8 (𝑥𝑦𝑦𝑥)
3 breq1 4008 . . . . . . . . . . . . . . 15 (𝑦 = ∅ → (𝑦𝑥 ↔ ∅ ≈ 𝑥))
43anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥)))
54imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = ∅ → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
65albidv 1824 . . . . . . . . . . . 12 (𝑦 = ∅ → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)))
7 breq1 4008 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
87anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥)))
98imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
109albidv 1824 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)))
11 breq1 4008 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑣 → (𝑦𝑥 ↔ suc 𝑣𝑥))
1211anbi2d 464 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑣 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥)))
1312imbi1d 231 . . . . . . . . . . . . 13 (𝑦 = suc 𝑣 → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
1413albidv 1824 . . . . . . . . . . . 12 (𝑦 = suc 𝑣 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) ↔ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
15 ensym 6784 . . . . . . . . . . . . . . . . . . 19 (∅ ≈ 𝑥𝑥 ≈ ∅)
16 en0 6798 . . . . . . . . . . . . . . . . . . 19 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
1715, 16sylib 122 . . . . . . . . . . . . . . . . . 18 (∅ ≈ 𝑥𝑥 = ∅)
1817anim1i 340 . . . . . . . . . . . . . . . . 17 ((∅ ≈ 𝑥𝑥 ≠ ∅) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
1918ancoms 268 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
2019adantll 476 . . . . . . . . . . . . . . 15 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → (𝑥 = ∅ ∧ 𝑥 ≠ ∅))
21 df-ne 2348 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
22 pm3.24 693 . . . . . . . . . . . . . . . . 17 ¬ (𝑥 = ∅ ∧ ¬ 𝑥 = ∅)
2322pm2.21i 646 . . . . . . . . . . . . . . . 16 ((𝑥 = ∅ ∧ ¬ 𝑥 = ∅) → 𝑥𝐴)
2421, 23sylan2b 287 . . . . . . . . . . . . . . 15 ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → 𝑥𝐴)
2520, 24syl 14 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2625ax-gen 1449 . . . . . . . . . . . . 13 𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴)
2726a1i 9 . . . . . . . . . . . 12 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ ∅ ≈ 𝑥) → 𝑥𝐴))
28 nfv 1528 . . . . . . . . . . . . . 14 𝑥(𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
29 nfa1 1541 . . . . . . . . . . . . . 14 𝑥𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)
30 simpl 109 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ≠ ∅) → 𝑥𝐴)
31 bren 6750 . . . . . . . . . . . . . . . . . . 19 (suc 𝑣𝑥 ↔ ∃𝑓 𝑓:suc 𝑣1-1-onto𝑥)
32 ssel 3151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐴 → ((𝑓𝑣) ∈ 𝑥 → (𝑓𝑣) ∈ 𝐴))
33 f1of 5463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣𝑥)
34 vex 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑣 ∈ V
3534sucid 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑣 ∈ suc 𝑣
36 ffvelcdm 5652 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4968 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑣 = ∅ → (𝑓𝑣) = (𝑓 “ ∅))
42 ima0 4989 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 “ ∅) = ∅
4341, 42eqtrdi 2226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = ∅ → (𝑓𝑣) = ∅)
44 inteq 3849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑣) = ∅ → (𝑓𝑣) = ∅)
45 int0 3860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ∅ = V
4644, 45eqtrdi 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) = ∅ → (𝑓𝑣) = V)
4746ineq1d 3337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (V ∩ (𝑓𝑣)))
48 ssv 3179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓𝑣) ⊆ V
49 sseqin2 3356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓𝑣) ⊆ V ↔ (V ∩ (𝑓𝑣)) = (𝑓𝑣))
5048, 49mpbi 145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (V ∩ (𝑓𝑣)) = (𝑓𝑣)
5147, 50eqtrdi 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) = ∅ → ( (𝑓𝑣) ∩ (𝑓𝑣)) = (𝑓𝑣))
5251eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓𝑣) = ∅ → (( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴 ↔ (𝑓𝑣) ∈ 𝐴))
5352biimprd 158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓𝑣) = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ∅ → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
5554adantl 277 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ 𝑣 = ∅) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
56 f1ofun 5465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → Fun 𝑓)
5756ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → Fun 𝑓)
58 elelsuc 4411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∅ ∈ 𝑣 → ∅ ∈ suc 𝑣)
5958adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → ∅ ∈ suc 𝑣)
60 f1odm 5467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:suc 𝑣1-1-onto𝑥 → dom 𝑓 = suc 𝑣)
6160eleq2d 2247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝑓 ∧ ∅ ∈ dom 𝑓) → (∅ ∈ 𝑣 → (𝑓‘∅) ∈ (𝑓𝑣)))
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓‘∅) ∈ (𝑓𝑣))
68 ne0i 3431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓‘∅) ∈ (𝑓𝑣) → (𝑓𝑣) ≠ ∅)
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) ∧ ∅ ∈ 𝑣) → (𝑓𝑣) ≠ ∅)
70 imassrn 4983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓𝑣) ⊆ ran 𝑓
71 dff1o2 5468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:suc 𝑣1-1-onto𝑥 ↔ (𝑓 Fn suc 𝑣 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑥))
7271simp3bi 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:suc 𝑣1-1-onto𝑥 → ran 𝑓 = 𝑥)
7370, 72sseqtrid 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓𝑣) ⊆ 𝑥)
74 sstr2 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓𝑣) ⊆ 𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑥𝐴 → (𝑓𝑣) ⊆ 𝐴))
7675anim1d 336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
77 f1of1 5462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣1-1𝑥)
78 vex 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑥 ∈ V
79 sssucid 4417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 ⊆ suc 𝑣
80 f1imaen2g 6796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓:suc 𝑣1-1-onto𝑥𝑣 ≈ (𝑓𝑣))
8476, 83jctird 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
85 vex 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑓 ∈ V
8685imaex 4985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓𝑣) ∈ V
87 sseq1 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥𝐴 ↔ (𝑓𝑣) ⊆ 𝐴))
88 neeq1 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑓𝑣) → (𝑥 ≠ ∅ ↔ (𝑓𝑣) ≠ ∅))
8987, 88anbi12d 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → ((𝑥𝐴𝑥 ≠ ∅) ↔ ((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅)))
90 breq2 4009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → (𝑣𝑥𝑣 ≈ (𝑓𝑣)))
9189, 90anbi12d 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) ↔ (((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣))))
92 inteq 3849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑥 = (𝑓𝑣) → 𝑥 = (𝑓𝑣))
9392eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑓𝑣) → ( 𝑥𝐴 (𝑓𝑣) ∈ 𝐴))
9491, 93imbi12d 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑓𝑣) → ((((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ↔ ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴)))
9586, 94spcv 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ((((𝑓𝑣) ⊆ 𝐴 ∧ (𝑓𝑣) ≠ ∅) ∧ 𝑣 ≈ (𝑓𝑣)) → (𝑓𝑣) ∈ 𝐴))
9684, 95sylan9 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓:suc 𝑣1-1-onto𝑥 ∧ ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴)) → ((𝑥𝐴 ∧ (𝑓𝑣) ≠ ∅) → (𝑓𝑣) ∈ 𝐴))
97 ineq1 3331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝑓𝑣) → (𝑧𝑤) = ( (𝑓𝑣) ∩ 𝑤))
9897eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝑓𝑣) → ((𝑧𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴))
99 ineq2 3332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 = (𝑓𝑣) → ( (𝑓𝑣) ∩ 𝑤) = ( (𝑓𝑣) ∩ (𝑓𝑣)))
10099eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = (𝑓𝑣) → (( (𝑓𝑣) ∩ 𝑤) ∈ 𝐴 ↔ ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
10198, 100rspc2v 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4620 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
112111ad3antrrr 492 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
11355, 110, 112mpjaodan 798 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ((𝑓𝑣) ∈ 𝐴 → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴))
11440, 113mpd 13 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑣 ∈ ω ∧ 𝑥𝐴) ∧ 𝑓:suc 𝑣1-1-onto𝑥) ∧ (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)) → ( (𝑓𝑣) ∩ (𝑓𝑣)) ∈ 𝐴)
11585, 34fvex 5537 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓𝑣) ∈ V
116115intunsn 3884 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ( (𝑓𝑣) ∩ (𝑓𝑣))
117 f1ofn 5464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:suc 𝑣1-1-onto𝑥𝑓 Fn suc 𝑣)
118 fnsnfv 5578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 Fn suc 𝑣𝑣 ∈ suc 𝑣) → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
119117, 35, 118sylancl 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓:suc 𝑣1-1-onto𝑥 → {(𝑓𝑣)} = (𝑓 “ {𝑣}))
120119uneq2d 3291 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣})))
121 df-suc 4373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑣 = (𝑣 ∪ {𝑣})
122121imaeq2i 4970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ suc 𝑣) = (𝑓 “ (𝑣 ∪ {𝑣}))
123 imaundi 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 “ (𝑣 ∪ {𝑣})) = ((𝑓𝑣) ∪ (𝑓 “ {𝑣}))
124122, 123eqtr2i 2199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑣) ∪ (𝑓 “ {𝑣})) = (𝑓 “ suc 𝑣)
125120, 124eqtrdi 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = (𝑓 “ suc 𝑣))
126 f1ofo 5470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣1-1-onto𝑥𝑓:suc 𝑣onto𝑥)
127 foima 5445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:suc 𝑣onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:suc 𝑣1-1-onto𝑥 → (𝑓 “ suc 𝑣) = 𝑥)
129125, 128eqtrd 2210 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:suc 𝑣1-1-onto𝑥 → ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
130129inteqd 3851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:suc 𝑣1-1-onto𝑥 ((𝑓𝑣) ∪ {(𝑓𝑣)}) = 𝑥)
131116, 130eqtr3id 2224 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:suc 𝑣1-1-onto𝑥 → ( (𝑓𝑣) ∩ (𝑓𝑣)) = 𝑥)
132131eleq1d 2246 . . . . . . . . . . . . . . . . . . . . . . 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 1819 . . . . . . . . . . . . . . . . . . 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 1610 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴) → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴)))
143142ex 115 . . . . . . . . . . . 12 (𝑣 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑣𝑥) → 𝑥𝐴) → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ suc 𝑣𝑥) → 𝑥𝐴))))
1446, 10, 14, 27, 143finds2 4602 . . . . . . . . . . 11 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
145 sp 1511 . . . . . . . . . . 11 (∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴) → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴))
146144, 145syl6 33 . . . . . . . . . 10 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑦𝑥) → 𝑥𝐴)))
147146exp4a 366 . . . . . . . . 9 (𝑦 ∈ ω → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑦𝑥 𝑥𝐴))))
148147com24 87 . . . . . . . 8 (𝑦 ∈ ω → (𝑦𝑥 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
1492, 148syl5 32 . . . . . . 7 (𝑦 ∈ ω → (𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴))))
150149rexlimiv 2588 . . . . . 6 (∃𝑦 ∈ ω 𝑥𝑦 → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
1511, 150sylbi 121 . . . . 5 (𝑥 ∈ Fin → ((𝑥𝐴𝑥 ≠ ∅) → (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 𝑥𝐴)))
152151com13 80 . . . 4 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ((𝑥𝐴𝑥 ≠ ∅) → (𝑥 ∈ Fin → 𝑥𝐴)))
153152impd 254 . . 3 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
154153alrimiv 1874 . 2 (∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴 → ∀𝑥(((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
155 ineq1 3331 . . . 4 (𝑥 = 𝑧 → (𝑥𝑦) = (𝑧𝑦))
156155eleq1d 2246 . . 3 (𝑥 = 𝑧 → ((𝑥𝑦) ∈ 𝐴 ↔ (𝑧𝑦) ∈ 𝐴))
157 ineq2 3332 . . . 4 (𝑦 = 𝑤 → (𝑧𝑦) = (𝑧𝑤))
158157eleq1d 2246 . . 3 (𝑦 = 𝑤 → ((𝑧𝑦) ∈ 𝐴 ↔ (𝑧𝑤) ∈ 𝐴))
159156, 158cbvral2v 2718 . 2 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦) ∈ 𝐴 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧𝑤) ∈ 𝐴)
160 df-3an 980 . . . 4 ((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin))
161160imbi1i 238 . . 3 (((𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐴) ↔ (((𝑥𝐴𝑥 ≠ ∅) ∧ 𝑥 ∈ Fin) → 𝑥𝐴))
162161albii 1470 . 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 708  w3a 978  wal 1351   = wceq 1353  wex 1492  wcel 2148  wne 2347  wral 2455  wrex 2456  Vcvv 2739  cun 3129  cin 3130  wss 3131  c0 3424  {csn 3594   cint 3846   class class class wbr 4005  suc csuc 4367  ωcom 4591  ccnv 4627  dom cdm 4628  ran crn 4629  cima 4631  Fun wfun 5212   Fn wfn 5213  wf 5214  1-1wf1 5215  ontowfo 5216  1-1-ontowf1o 5217  cfv 5218  cen 6741  Fincfn 6743
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-id 4295  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-er 6538  df-en 6744  df-fin 6746
This theorem is referenced by:  istopfin  13688
  Copyright terms: Public domain W3C validator