Metamath Proof Explorer


Theorem fiint

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of A is in A ". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002)

Ref Expression
Assertion fiint ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )

Proof

Step Hyp Ref Expression
1 isfi ( 𝑥 ∈ Fin ↔ ∃ 𝑦 ∈ ω 𝑥𝑦 )
2 ensym ( 𝑥𝑦𝑦𝑥 )
3 breq1 ( 𝑦 = ∅ → ( 𝑦𝑥 ↔ ∅ ≈ 𝑥 ) )
4 3 anbi2d ( 𝑦 = ∅ → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) ) )
5 4 imbi1d ( 𝑦 = ∅ → ( ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ↔ ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → 𝑥𝐴 ) ) )
6 5 albidv ( 𝑦 = ∅ → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → 𝑥𝐴 ) ) )
7 breq1 ( 𝑦 = 𝑣 → ( 𝑦𝑥𝑣𝑥 ) )
8 7 anbi2d ( 𝑦 = 𝑣 → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) ) )
9 8 imbi1d ( 𝑦 = 𝑣 → ( ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ↔ ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ) )
10 9 albidv ( 𝑦 = 𝑣 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ) )
11 breq1 ( 𝑦 = suc 𝑣 → ( 𝑦𝑥 ↔ suc 𝑣𝑥 ) )
12 11 anbi2d ( 𝑦 = suc 𝑣 → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) ) )
13 12 imbi1d ( 𝑦 = suc 𝑣 → ( ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ↔ ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) → 𝑥𝐴 ) ) )
14 13 albidv ( 𝑦 = suc 𝑣 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) → 𝑥𝐴 ) ) )
15 ensym ( ∅ ≈ 𝑥𝑥 ≈ ∅ )
16 en0 ( 𝑥 ≈ ∅ ↔ 𝑥 = ∅ )
17 15 16 sylib ( ∅ ≈ 𝑥𝑥 = ∅ )
18 17 anim1i ( ( ∅ ≈ 𝑥𝑥 ≠ ∅ ) → ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) )
19 18 ancoms ( ( 𝑥 ≠ ∅ ∧ ∅ ≈ 𝑥 ) → ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) )
20 19 adantll ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) )
21 df-ne ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅ )
22 pm3.24 ¬ ( 𝑥 = ∅ ∧ ¬ 𝑥 = ∅ )
23 22 pm2.21i ( ( 𝑥 = ∅ ∧ ¬ 𝑥 = ∅ ) → 𝑥𝐴 )
24 21 23 sylan2b ( ( 𝑥 = ∅ ∧ 𝑥 ≠ ∅ ) → 𝑥𝐴 )
25 20 24 syl ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → 𝑥𝐴 )
26 25 ax-gen 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → 𝑥𝐴 )
27 26 a1i ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ ∅ ≈ 𝑥 ) → 𝑥𝐴 ) )
28 nfv 𝑥𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴
29 nfa1 𝑥𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 )
30 bren ( suc 𝑣𝑥 ↔ ∃ 𝑓 𝑓 : suc 𝑣1-1-onto𝑥 )
31 ssel ( 𝑥𝐴 → ( ( 𝑓𝑣 ) ∈ 𝑥 → ( 𝑓𝑣 ) ∈ 𝐴 ) )
32 f1of ( 𝑓 : suc 𝑣1-1-onto𝑥𝑓 : suc 𝑣𝑥 )
33 vex 𝑣 ∈ V
34 33 sucid 𝑣 ∈ suc 𝑣
35 ffvelrn ( ( 𝑓 : suc 𝑣𝑥𝑣 ∈ suc 𝑣 ) → ( 𝑓𝑣 ) ∈ 𝑥 )
36 32 34 35 sylancl ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( 𝑓𝑣 ) ∈ 𝑥 )
37 31 36 impel ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) → ( 𝑓𝑣 ) ∈ 𝐴 )
38 37 adantr ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → ( 𝑓𝑣 ) ∈ 𝐴 )
39 df-ne ( ( 𝑓𝑣 ) ≠ ∅ ↔ ¬ ( 𝑓𝑣 ) = ∅ )
40 imassrn ( 𝑓𝑣 ) ⊆ ran 𝑓
41 dff1o2 ( 𝑓 : suc 𝑣1-1-onto𝑥 ↔ ( 𝑓 Fn suc 𝑣 ∧ Fun 𝑓 ∧ ran 𝑓 = 𝑥 ) )
42 41 simp3bi ( 𝑓 : suc 𝑣1-1-onto𝑥 → ran 𝑓 = 𝑥 )
43 40 42 sseqtrid ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( 𝑓𝑣 ) ⊆ 𝑥 )
44 sstr2 ( ( 𝑓𝑣 ) ⊆ 𝑥 → ( 𝑥𝐴 → ( 𝑓𝑣 ) ⊆ 𝐴 ) )
45 43 44 syl ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( 𝑥𝐴 → ( 𝑓𝑣 ) ⊆ 𝐴 ) )
46 45 anim1d ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( 𝑥𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) → ( ( 𝑓𝑣 ) ⊆ 𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) ) )
47 f1of1 ( 𝑓 : suc 𝑣1-1-onto𝑥𝑓 : suc 𝑣1-1𝑥 )
48 vex 𝑥 ∈ V
49 sssucid 𝑣 ⊆ suc 𝑣
50 f1imaen2g ( ( ( 𝑓 : suc 𝑣1-1𝑥𝑥 ∈ V ) ∧ ( 𝑣 ⊆ suc 𝑣𝑣 ∈ V ) ) → ( 𝑓𝑣 ) ≈ 𝑣 )
51 49 33 50 mpanr12 ( ( 𝑓 : suc 𝑣1-1𝑥𝑥 ∈ V ) → ( 𝑓𝑣 ) ≈ 𝑣 )
52 47 48 51 sylancl ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( 𝑓𝑣 ) ≈ 𝑣 )
53 52 ensymd ( 𝑓 : suc 𝑣1-1-onto𝑥𝑣 ≈ ( 𝑓𝑣 ) )
54 46 53 jctird ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( 𝑥𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) → ( ( ( 𝑓𝑣 ) ⊆ 𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓𝑣 ) ) ) )
55 vex 𝑓 ∈ V
56 55 imaex ( 𝑓𝑣 ) ∈ V
57 sseq1 ( 𝑥 = ( 𝑓𝑣 ) → ( 𝑥𝐴 ↔ ( 𝑓𝑣 ) ⊆ 𝐴 ) )
58 neeq1 ( 𝑥 = ( 𝑓𝑣 ) → ( 𝑥 ≠ ∅ ↔ ( 𝑓𝑣 ) ≠ ∅ ) )
59 57 58 anbi12d ( 𝑥 = ( 𝑓𝑣 ) → ( ( 𝑥𝐴𝑥 ≠ ∅ ) ↔ ( ( 𝑓𝑣 ) ⊆ 𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) ) )
60 breq2 ( 𝑥 = ( 𝑓𝑣 ) → ( 𝑣𝑥𝑣 ≈ ( 𝑓𝑣 ) ) )
61 59 60 anbi12d ( 𝑥 = ( 𝑓𝑣 ) → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) ↔ ( ( ( 𝑓𝑣 ) ⊆ 𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓𝑣 ) ) ) )
62 inteq ( 𝑥 = ( 𝑓𝑣 ) → 𝑥 = ( 𝑓𝑣 ) )
63 62 eleq1d ( 𝑥 = ( 𝑓𝑣 ) → ( 𝑥𝐴 ( 𝑓𝑣 ) ∈ 𝐴 ) )
64 61 63 imbi12d ( 𝑥 = ( 𝑓𝑣 ) → ( ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ↔ ( ( ( ( 𝑓𝑣 ) ⊆ 𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓𝑣 ) ) → ( 𝑓𝑣 ) ∈ 𝐴 ) ) )
65 56 64 spcv ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ( ( ( 𝑓𝑣 ) ⊆ 𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) ∧ 𝑣 ≈ ( 𝑓𝑣 ) ) → ( 𝑓𝑣 ) ∈ 𝐴 ) )
66 54 65 sylan9 ( ( 𝑓 : suc 𝑣1-1-onto𝑥 ∧ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ) → ( ( 𝑥𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) → ( 𝑓𝑣 ) ∈ 𝐴 ) )
67 ineq1 ( 𝑧 = ( 𝑓𝑣 ) → ( 𝑧𝑤 ) = ( ( 𝑓𝑣 ) ∩ 𝑤 ) )
68 67 eleq1d ( 𝑧 = ( 𝑓𝑣 ) → ( ( 𝑧𝑤 ) ∈ 𝐴 ↔ ( ( 𝑓𝑣 ) ∩ 𝑤 ) ∈ 𝐴 ) )
69 ineq2 ( 𝑤 = ( 𝑓𝑣 ) → ( ( 𝑓𝑣 ) ∩ 𝑤 ) = ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) )
70 69 eleq1d ( 𝑤 = ( 𝑓𝑣 ) → ( ( ( 𝑓𝑣 ) ∩ 𝑤 ) ∈ 𝐴 ↔ ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) )
71 68 70 rspc2v ( ( ( 𝑓𝑣 ) ∈ 𝐴 ∧ ( 𝑓𝑣 ) ∈ 𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) )
72 71 ex ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) )
73 66 72 syl6 ( ( 𝑓 : suc 𝑣1-1-onto𝑥 ∧ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ) → ( ( 𝑥𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) ) )
74 73 com4r ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑓 : suc 𝑣1-1-onto𝑥 ∧ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ) → ( ( 𝑥𝐴 ∧ ( 𝑓𝑣 ) ≠ ∅ ) → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) ) )
75 74 exp5c ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( 𝑥𝐴 → ( ( 𝑓𝑣 ) ≠ ∅ → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) ) ) ) )
76 75 com14 ( 𝑥𝐴 → ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ≠ ∅ → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) ) ) ) )
77 76 imp43 ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → ( ( 𝑓𝑣 ) ≠ ∅ → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) )
78 39 77 syl5bir ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → ( ¬ ( 𝑓𝑣 ) = ∅ → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) ) )
79 inteq ( ( 𝑓𝑣 ) = ∅ → ( 𝑓𝑣 ) = ∅ )
80 int0 ∅ = V
81 79 80 eqtrdi ( ( 𝑓𝑣 ) = ∅ → ( 𝑓𝑣 ) = V )
82 81 ineq1d ( ( 𝑓𝑣 ) = ∅ → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) = ( V ∩ ( 𝑓𝑣 ) ) )
83 ssv ( 𝑓𝑣 ) ⊆ V
84 sseqin2 ( ( 𝑓𝑣 ) ⊆ V ↔ ( V ∩ ( 𝑓𝑣 ) ) = ( 𝑓𝑣 ) )
85 83 84 mpbi ( V ∩ ( 𝑓𝑣 ) ) = ( 𝑓𝑣 )
86 82 85 eqtrdi ( ( 𝑓𝑣 ) = ∅ → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) = ( 𝑓𝑣 ) )
87 86 eleq1d ( ( 𝑓𝑣 ) = ∅ → ( ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ↔ ( 𝑓𝑣 ) ∈ 𝐴 ) )
88 87 biimprd ( ( 𝑓𝑣 ) = ∅ → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) )
89 78 88 pm2.61d2 ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → ( ( 𝑓𝑣 ) ∈ 𝐴 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 ) )
90 38 89 mpd ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 )
91 fvex ( 𝑓𝑣 ) ∈ V
92 91 intunsn ( ( 𝑓𝑣 ) ∪ { ( 𝑓𝑣 ) } ) = ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) )
93 f1ofn ( 𝑓 : suc 𝑣1-1-onto𝑥𝑓 Fn suc 𝑣 )
94 fnsnfv ( ( 𝑓 Fn suc 𝑣𝑣 ∈ suc 𝑣 ) → { ( 𝑓𝑣 ) } = ( 𝑓 “ { 𝑣 } ) )
95 93 34 94 sylancl ( 𝑓 : suc 𝑣1-1-onto𝑥 → { ( 𝑓𝑣 ) } = ( 𝑓 “ { 𝑣 } ) )
96 95 uneq2d ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( 𝑓𝑣 ) ∪ { ( 𝑓𝑣 ) } ) = ( ( 𝑓𝑣 ) ∪ ( 𝑓 “ { 𝑣 } ) ) )
97 df-suc suc 𝑣 = ( 𝑣 ∪ { 𝑣 } )
98 97 imaeq2i ( 𝑓 “ suc 𝑣 ) = ( 𝑓 “ ( 𝑣 ∪ { 𝑣 } ) )
99 imaundi ( 𝑓 “ ( 𝑣 ∪ { 𝑣 } ) ) = ( ( 𝑓𝑣 ) ∪ ( 𝑓 “ { 𝑣 } ) )
100 98 99 eqtr2i ( ( 𝑓𝑣 ) ∪ ( 𝑓 “ { 𝑣 } ) ) = ( 𝑓 “ suc 𝑣 )
101 96 100 eqtrdi ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( 𝑓𝑣 ) ∪ { ( 𝑓𝑣 ) } ) = ( 𝑓 “ suc 𝑣 ) )
102 f1ofo ( 𝑓 : suc 𝑣1-1-onto𝑥𝑓 : suc 𝑣onto𝑥 )
103 foima ( 𝑓 : suc 𝑣onto𝑥 → ( 𝑓 “ suc 𝑣 ) = 𝑥 )
104 102 103 syl ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( 𝑓 “ suc 𝑣 ) = 𝑥 )
105 101 104 eqtrd ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( 𝑓𝑣 ) ∪ { ( 𝑓𝑣 ) } ) = 𝑥 )
106 105 inteqd ( 𝑓 : suc 𝑣1-1-onto𝑥 ( ( 𝑓𝑣 ) ∪ { ( 𝑓𝑣 ) } ) = 𝑥 )
107 92 106 eqtr3id ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) = 𝑥 )
108 107 eleq1d ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 𝑥𝐴 ) )
109 108 ad2antlr ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → ( ( ( 𝑓𝑣 ) ∩ ( 𝑓𝑣 ) ) ∈ 𝐴 𝑥𝐴 ) )
110 90 109 mpbid ( ( ( 𝑥𝐴𝑓 : suc 𝑣1-1-onto𝑥 ) ∧ ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ) ) → 𝑥𝐴 )
111 110 exp43 ( 𝑥𝐴 → ( 𝑓 : suc 𝑣1-1-onto𝑥 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) ) )
112 111 exlimdv ( 𝑥𝐴 → ( ∃ 𝑓 𝑓 : suc 𝑣1-1-onto𝑥 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) ) )
113 30 112 syl5bi ( 𝑥𝐴 → ( suc 𝑣𝑥 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) ) )
114 113 imp ( ( 𝑥𝐴 ∧ suc 𝑣𝑥 ) → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) )
115 114 adantlr ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) )
116 115 com13 ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) → 𝑥𝐴 ) ) )
117 28 29 116 alrimd ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) → 𝑥𝐴 ) ) )
118 117 a1i ( 𝑣 ∈ ω → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑣𝑥 ) → 𝑥𝐴 ) → ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ suc 𝑣𝑥 ) → 𝑥𝐴 ) ) ) )
119 6 10 14 27 118 finds2 ( 𝑦 ∈ ω → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ) )
120 sp ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) )
121 119 120 syl6 ( 𝑦 ∈ ω → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑦𝑥 ) → 𝑥𝐴 ) ) )
122 121 exp4a ( 𝑦 ∈ ω → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ( 𝑦𝑥 𝑥𝐴 ) ) ) )
123 122 com24 ( 𝑦 ∈ ω → ( 𝑦𝑥 → ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) ) )
124 2 123 syl5 ( 𝑦 ∈ ω → ( 𝑥𝑦 → ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) ) )
125 124 rexlimiv ( ∃ 𝑦 ∈ ω 𝑥𝑦 → ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) )
126 1 125 sylbi ( 𝑥 ∈ Fin → ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 𝑥𝐴 ) ) )
127 126 com13 ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( 𝑥𝐴𝑥 ≠ ∅ ) → ( 𝑥 ∈ Fin → 𝑥𝐴 ) ) )
128 127 impd ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )
129 128 alrimiv ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 → ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )
130 zfpair2 { 𝑧 , 𝑤 } ∈ V
131 sseq1 ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥𝐴 ↔ { 𝑧 , 𝑤 } ⊆ 𝐴 ) )
132 neeq1 ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥 ≠ ∅ ↔ { 𝑧 , 𝑤 } ≠ ∅ ) )
133 131 132 anbi12d ( 𝑥 = { 𝑧 , 𝑤 } → ( ( 𝑥𝐴𝑥 ≠ ∅ ) ↔ ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ) )
134 eleq1 ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥 ∈ Fin ↔ { 𝑧 , 𝑤 } ∈ Fin ) )
135 133 134 anbi12d ( 𝑥 = { 𝑧 , 𝑤 } → ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) ↔ ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) ) )
136 inteq ( 𝑥 = { 𝑧 , 𝑤 } → 𝑥 = { 𝑧 , 𝑤 } )
137 136 eleq1d ( 𝑥 = { 𝑧 , 𝑤 } → ( 𝑥𝐴 { 𝑧 , 𝑤 } ∈ 𝐴 ) )
138 135 137 imbi12d ( 𝑥 = { 𝑧 , 𝑤 } → ( ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) ↔ ( ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) → { 𝑧 , 𝑤 } ∈ 𝐴 ) ) )
139 130 138 spcv ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) → ( ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) → { 𝑧 , 𝑤 } ∈ 𝐴 ) )
140 vex 𝑧 ∈ V
141 vex 𝑤 ∈ V
142 140 141 prss ( ( 𝑧𝐴𝑤𝐴 ) ↔ { 𝑧 , 𝑤 } ⊆ 𝐴 )
143 140 prnz { 𝑧 , 𝑤 } ≠ ∅
144 143 biantru ( { 𝑧 , 𝑤 } ⊆ 𝐴 ↔ ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) )
145 prfi { 𝑧 , 𝑤 } ∈ Fin
146 145 biantru ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ↔ ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) )
147 142 144 146 3bitrri ( ( ( { 𝑧 , 𝑤 } ⊆ 𝐴 ∧ { 𝑧 , 𝑤 } ≠ ∅ ) ∧ { 𝑧 , 𝑤 } ∈ Fin ) ↔ ( 𝑧𝐴𝑤𝐴 ) )
148 140 141 intpr { 𝑧 , 𝑤 } = ( 𝑧𝑤 )
149 148 eleq1i ( { 𝑧 , 𝑤 } ∈ 𝐴 ↔ ( 𝑧𝑤 ) ∈ 𝐴 )
150 139 147 149 3imtr3g ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) → ( ( 𝑧𝐴𝑤𝐴 ) → ( 𝑧𝑤 ) ∈ 𝐴 ) )
151 150 ralrimivv ( ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) → ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 )
152 129 151 impbii ( ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 ↔ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )
153 ineq1 ( 𝑥 = 𝑧 → ( 𝑥𝑦 ) = ( 𝑧𝑦 ) )
154 153 eleq1d ( 𝑥 = 𝑧 → ( ( 𝑥𝑦 ) ∈ 𝐴 ↔ ( 𝑧𝑦 ) ∈ 𝐴 ) )
155 ineq2 ( 𝑦 = 𝑤 → ( 𝑧𝑦 ) = ( 𝑧𝑤 ) )
156 155 eleq1d ( 𝑦 = 𝑤 → ( ( 𝑧𝑦 ) ∈ 𝐴 ↔ ( 𝑧𝑤 ) ∈ 𝐴 ) )
157 154 156 cbvral2vw ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 ↔ ∀ 𝑧𝐴𝑤𝐴 ( 𝑧𝑤 ) ∈ 𝐴 )
158 df-3an ( ( 𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ↔ ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) )
159 158 imbi1i ( ( ( 𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) ↔ ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )
160 159 albii ( ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥𝐴𝑥 ≠ ∅ ) ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )
161 152 157 160 3bitr4i ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐴 ) )