Metamath Proof Explorer

Theorem fineqvac

Description: If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep and ax-pow , see fineqvacALT . (Contributed by BTernaryTau, 21-Sep-2024)

Ref Expression
Assertion fineqvac ( Fin = V → CHOICE )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑤 ∈ V
2 eleq2w2 ⊢ ( Fin = V → ( 𝑤 ∈ Fin ↔ 𝑤 ∈ V ) )
3 1 2 mpbiri ⊢ ( Fin = V → 𝑤 ∈ Fin )
4 sseq2 ⊢ ( 𝑥 = ∅ → ( 𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅ ) )
5 dmeq ⊢ ( 𝑥 = ∅ → dom 𝑥 = dom ∅ )
6 5 fneq2d ⊢ ( 𝑥 = ∅ → ( 𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅ ) )
7 4 6 anbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ( 𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅ ) ) )
8 7 exbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅ ) ) )
9 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦 ) )
10 dmeq ⊢ ( 𝑥 = 𝑦 → dom 𝑥 = dom 𝑦 )
11 10 fneq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦 ) )
12 9 11 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ) )
13 12 exbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ) )
14 sseq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) )
15 dmeq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → dom 𝑥 = dom ( 𝑦 ∪ { 𝑧 } ) )
16 15 fneq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
17 14 16 anbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
18 17 exbidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
19 sseq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤 ) )
20 dmeq ⊢ ( 𝑥 = 𝑤 → dom 𝑥 = dom 𝑤 )
21 20 fneq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤 ) )
22 19 21 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ( 𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤 ) ) )
23 22 exbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤 ) ) )
24 ssid ⊢ ∅ ⊆ ∅
25 fun0 ⊢ Fun ∅
26 funfn ⊢ ( Fun ∅ ↔ ∅ Fn dom ∅ )
27 25 26 mpbi ⊢ ∅ Fn dom ∅
28 0ex ⊢ ∅ ∈ V
29 sseq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 ⊆ ∅ ↔ ∅ ⊆ ∅ ) )
30 fneq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 Fn dom ∅ ↔ ∅ Fn dom ∅ ) )
31 29 30 anbi12d ⊢ ( 𝑓 = ∅ → ( ( 𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅ ) ↔ ( ∅ ⊆ ∅ ∧ ∅ Fn dom ∅ ) ) )
32 28 31 spcev ⊢ ( ( ∅ ⊆ ∅ ∧ ∅ Fn dom ∅ ) → ∃ 𝑓 ( 𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅ ) )
33 24 27 32 mp2an ⊢ ∃ 𝑓 ( 𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅ )
34 sseq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦 ) )
35 fneq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦 ) )
36 34 35 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ↔ ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ) )
37 36 cbvexvw ⊢ ( ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) ↔ ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) )
38 ssun3 ⊢ ( 𝑔 ⊆ 𝑦 → 𝑔 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
39 38 ad2antrr ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ dom { 𝑧 } = ∅ ) → 𝑔 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
40 dmun ⊢ dom ( 𝑦 ∪ { 𝑧 } ) = ( dom 𝑦 ∪ dom { 𝑧 } )
41 uneq2 ⊢ ( dom { 𝑧 } = ∅ → ( dom 𝑦 ∪ dom { 𝑧 } ) = ( dom 𝑦 ∪ ∅ ) )
42 un0 ⊢ ( dom 𝑦 ∪ ∅ ) = dom 𝑦
43 41 42 eqtrdi ⊢ ( dom { 𝑧 } = ∅ → ( dom 𝑦 ∪ dom { 𝑧 } ) = dom 𝑦 )
44 40 43 syl5eq ⊢ ( dom { 𝑧 } = ∅ → dom ( 𝑦 ∪ { 𝑧 } ) = dom 𝑦 )
45 44 fneq2d ⊢ ( dom { 𝑧 } = ∅ → ( 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 Fn dom 𝑦 ) )
46 45 biimparc ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ dom { 𝑧 } = ∅ ) → 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) )
47 46 adantll ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ dom { 𝑧 } = ∅ ) → 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) )
48 vex ⊢ 𝑔 ∈ V
49 sseq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) )
50 fneq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
51 49 50 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ↔ ( 𝑔 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
52 48 51 spcev ⊢ ( ( 𝑔 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
53 39 47 52 syl2anc ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ dom { 𝑧 } = ∅ ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
54 dmsnn0 ⊢ ( 𝑧 ∈ ( V × V ) ↔ dom { 𝑧 } ≠ ∅ )
55 elvv ⊢ ( 𝑧 ∈ ( V × V ) ↔ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
56 54 55 bitr3i ⊢ ( dom { 𝑧 } ≠ ∅ ↔ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
57 56 anbi2i ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ dom { 𝑧 } ≠ ∅ ) ↔ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
58 19.42vv ⊢ ( ∃ 𝑢 ∃ 𝑣 ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) ↔ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
59 57 58 bitr4i ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ dom { 𝑧 } ≠ ∅ ) ↔ ∃ 𝑢 ∃ 𝑣 ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
60 38 3ad2ant1 ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → 𝑔 ⊆ ( 𝑦 ∪ { 𝑧 } ) )
61 snssi ⊢ ( 𝑢 ∈ dom 𝑦 → { 𝑢 } ⊆ dom 𝑦 )
62 ssequn2 ⊢ ( { 𝑢 } ⊆ dom 𝑦 ↔ ( dom 𝑦 ∪ { 𝑢 } ) = dom 𝑦 )
63 61 62 sylib ⊢ ( 𝑢 ∈ dom 𝑦 → ( dom 𝑦 ∪ { 𝑢 } ) = dom 𝑦 )
64 63 fneq2d ⊢ ( 𝑢 ∈ dom 𝑦 → ( 𝑔 Fn ( dom 𝑦 ∪ { 𝑢 } ) ↔ 𝑔 Fn dom 𝑦 ) )
65 64 biimparc ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦 ) → 𝑔 Fn ( dom 𝑦 ∪ { 𝑢 } ) )
66 65 3adant2 ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 ∈ dom 𝑦 ) → 𝑔 Fn ( dom 𝑦 ∪ { 𝑢 } ) )
67 sneq ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → { 𝑧 } = { ⟨ 𝑢 , 𝑣 ⟩ } )
68 67 dmeqd ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → dom { 𝑧 } = dom { ⟨ 𝑢 , 𝑣 ⟩ } )
69 vex ⊢ 𝑣 ∈ V
70 69 dmsnop ⊢ dom { ⟨ 𝑢 , 𝑣 ⟩ } = { 𝑢 }
71 68 70 eqtrdi ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → dom { 𝑧 } = { 𝑢 } )
72 71 uneq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( dom 𝑦 ∪ dom { 𝑧 } ) = ( dom 𝑦 ∪ { 𝑢 } ) )
73 40 72 syl5eq ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → dom ( 𝑦 ∪ { 𝑧 } ) = ( dom 𝑦 ∪ { 𝑢 } ) )
74 73 fneq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 Fn ( dom 𝑦 ∪ { 𝑢 } ) ) )
75 74 3ad2ant2 ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 ∈ dom 𝑦 ) → ( 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 Fn ( dom 𝑦 ∪ { 𝑢 } ) ) )
76 66 75 mpbird ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ 𝑢 ∈ dom 𝑦 ) → 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) )
77 76 3expia ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑢 ∈ dom 𝑦 → 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
78 77 3adant1 ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑢 ∈ dom 𝑦 → 𝑔 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
79 60 78 52 syl6an ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑢 ∈ dom 𝑦 → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
80 67 uneq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑔 ∪ { 𝑧 } ) = ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) )
81 80 adantl ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑔 ∪ { 𝑧 } ) = ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) )
82 unss1 ⊢ ( 𝑔 ⊆ 𝑦 → ( 𝑔 ∪ { 𝑧 } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
83 82 adantr ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑔 ∪ { 𝑧 } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
84 81 83 eqsstrrd ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
85 84 3adant2 ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) )
86 vex ⊢ 𝑢 ∈ V
87 86 a1i ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦 ) → 𝑢 ∈ V )
88 69 a1i ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦 ) → 𝑣 ∈ V )
89 simpl ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦 ) → 𝑔 Fn dom 𝑦 )
90 eqid ⊢ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) = ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } )
91 eqid ⊢ ( dom 𝑦 ∪ { 𝑢 } ) = ( dom 𝑦 ∪ { 𝑢 } )
92 simpr ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦 ) → ¬ 𝑢 ∈ dom 𝑦 )
93 87 88 89 90 91 92 fnunop ⊢ ( ( 𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦 ) → ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn ( dom 𝑦 ∪ { 𝑢 } ) )
94 93 ex ⊢ ( 𝑔 Fn dom 𝑦 → ( ¬ 𝑢 ∈ dom 𝑦 → ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn ( dom 𝑦 ∪ { 𝑢 } ) ) )
95 94 3ad2ant2 ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( ¬ 𝑢 ∈ dom 𝑦 → ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn ( dom 𝑦 ∪ { 𝑢 } ) ) )
96 73 fneq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn ( dom 𝑦 ∪ { 𝑢 } ) ) )
97 96 3ad2ant3 ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn ( dom 𝑦 ∪ { 𝑢 } ) ) )
98 95 97 sylibrd ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( ¬ 𝑢 ∈ dom 𝑦 → ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
99 snex ⊢ { ⟨ 𝑢 , 𝑣 ⟩ } ∈ V
100 48 99 unex ⊢ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) ∈ V
101 sseq1 ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) → ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) ) )
102 fneq1 ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) → ( 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
103 101 102 anbi12d ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) → ( ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ↔ ( ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
104 100 103 spcev ⊢ ( ( ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ ( 𝑔 ∪ { ⟨ 𝑢 , 𝑣 ⟩ } ) Fn dom ( 𝑦 ∪ { 𝑧 } ) ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
105 85 98 104 syl6an ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( ¬ 𝑢 ∈ dom 𝑦 → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
106 79 105 pm2.61d ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
107 106 3expa ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
108 107 exlimivv ⊢ ( ∃ 𝑢 ∃ 𝑣 ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
109 59 108 sylbi ⊢ ( ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) ∧ dom { 𝑧 } ≠ ∅ ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
110 53 109 pm2.61dane ⊢ ( ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
111 110 exlimiv ⊢ ( ∃ 𝑔 ( 𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
112 37 111 sylbi ⊢ ( ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) )
113 112 a1i ⊢ ( 𝑦 ∈ Fin → ( ∃ 𝑓 ( 𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦 ) → ∃ 𝑓 ( 𝑓 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ 𝑓 Fn dom ( 𝑦 ∪ { 𝑧 } ) ) ) )
114 8 13 18 23 33 113 findcard2 ⊢ ( 𝑤 ∈ Fin → ∃ 𝑓 ( 𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤 ) )
115 3 114 syl ⊢ ( Fin = V → ∃ 𝑓 ( 𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤 ) )
116 115 alrimiv ⊢ ( Fin = V → ∀ 𝑤 ∃ 𝑓 ( 𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤 ) )
117 df-ac ⊢ ( CHOICE ↔ ∀ 𝑤 ∃ 𝑓 ( 𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤 ) )
118 116 117 sylibr ⊢ ( Fin = V → CHOICE )