Metamath Proof Explorer


Theorem fnchoice

Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Assertion fnchoice ( 𝐴 ∈ Fin → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 fneq2 ( 𝑤 = ∅ → ( 𝑓 Fn 𝑤𝑓 Fn ∅ ) )
2 raleq ( 𝑤 = ∅ → ( ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
3 1 2 anbi12d ( 𝑤 = ∅ → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
4 3 exbidv ( 𝑤 = ∅ → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
5 fneq2 ( 𝑤 = 𝑦 → ( 𝑓 Fn 𝑤𝑓 Fn 𝑦 ) )
6 raleq ( 𝑤 = 𝑦 → ( ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
7 5 6 anbi12d ( 𝑤 = 𝑦 → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
8 7 exbidv ( 𝑤 = 𝑦 → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
9 fneq2 ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑓 Fn 𝑤𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ) )
10 raleq ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
11 9 10 anbi12d ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
12 11 exbidv ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
13 fneq2 ( 𝑤 = 𝐴 → ( 𝑓 Fn 𝑤𝑓 Fn 𝐴 ) )
14 raleq ( 𝑤 = 𝐴 → ( ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
15 13 14 anbi12d ( 𝑤 = 𝐴 → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
16 15 exbidv ( 𝑤 = 𝐴 → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥𝑤 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
17 0ex ∅ ∈ V
18 fneq1 ( 𝑓 = ∅ → ( 𝑓 Fn ∅ ↔ ∅ Fn ∅ ) )
19 eqid ∅ = ∅
20 fn0 ( ∅ Fn ∅ ↔ ∅ = ∅ )
21 19 20 mpbir ∅ Fn ∅
22 17 18 21 ceqsexv2d 𝑓 𝑓 Fn ∅
23 ral0 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 )
24 22 23 exan 𝑓 ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
25 dffn2 ( 𝑓 Fn 𝑦𝑓 : 𝑦 ⟶ V )
26 25 biimpi ( 𝑓 Fn 𝑦𝑓 : 𝑦 ⟶ V )
27 26 ad2antrl ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → 𝑓 : 𝑦 ⟶ V )
28 vex 𝑧 ∈ V
29 28 a1i ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → 𝑧 ∈ V )
30 simpllr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ¬ 𝑧𝑦 )
31 vex 𝑤 ∈ V
32 31 a1i ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → 𝑤 ∈ V )
33 fsnunf ( ( 𝑓 : 𝑦 ⟶ V ∧ ( 𝑧 ∈ V ∧ ¬ 𝑧𝑦 ) ∧ 𝑤 ∈ V ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V )
34 27 29 30 32 33 syl121anc ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V )
35 dffn2 ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V )
36 34 35 sylibr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) )
37 simplr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → 𝑧 = ∅ )
38 simprr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
39 nfv 𝑥 ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 )
40 nfra1 𝑥𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 )
41 39 40 nfan 𝑥 ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
42 simpr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → 𝑥𝑦 )
43 simpllr ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ¬ 𝑧𝑦 )
44 43 adantr ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ¬ 𝑧𝑦 )
45 44 adantr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ¬ 𝑧𝑦 )
46 42 45 jca ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( 𝑥𝑦 ∧ ¬ 𝑧𝑦 ) )
47 nelne2 ( ( 𝑥𝑦 ∧ ¬ 𝑧𝑦 ) → 𝑥𝑧 )
48 47 necomd ( ( 𝑥𝑦 ∧ ¬ 𝑧𝑦 ) → 𝑧𝑥 )
49 46 48 syl ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → 𝑧𝑥 )
50 fvunsn ( 𝑧𝑥 → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = ( 𝑓𝑥 ) )
51 49 50 syl ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = ( 𝑓𝑥 ) )
52 simpllr ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
53 52 adantr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
54 simplr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → 𝑥 ≠ ∅ )
55 neeq1 ( 𝑢 = 𝑥 → ( 𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅ ) )
56 fveq2 ( 𝑢 = 𝑥 → ( 𝑓𝑢 ) = ( 𝑓𝑥 ) )
57 56 eleq1d ( 𝑢 = 𝑥 → ( ( 𝑓𝑢 ) ∈ 𝑢 ↔ ( 𝑓𝑥 ) ∈ 𝑢 ) )
58 eleq2w ( 𝑢 = 𝑥 → ( ( 𝑓𝑥 ) ∈ 𝑢 ↔ ( 𝑓𝑥 ) ∈ 𝑥 ) )
59 57 58 bitrd ( 𝑢 = 𝑥 → ( ( 𝑓𝑢 ) ∈ 𝑢 ↔ ( 𝑓𝑥 ) ∈ 𝑥 ) )
60 55 59 imbi12d ( 𝑢 = 𝑥 → ( ( 𝑢 ≠ ∅ → ( 𝑓𝑢 ) ∈ 𝑢 ) ↔ ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
61 60 cbvralvw ( ∀ 𝑢𝑦 ( 𝑢 ≠ ∅ → ( 𝑓𝑢 ) ∈ 𝑢 ) ↔ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
62 60 rspcv ( 𝑥𝑦 → ( ∀ 𝑢𝑦 ( 𝑢 ≠ ∅ → ( 𝑓𝑢 ) ∈ 𝑢 ) → ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
63 61 62 syl5bir ( 𝑥𝑦 → ( ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) → ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
64 42 53 54 63 syl3c ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( 𝑓𝑥 ) ∈ 𝑥 )
65 51 64 eqeltrd ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
66 simp-4l ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑧 = ∅ )
67 66 adantr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑧 = ∅ )
68 simpr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 ∈ { 𝑧 } )
69 simplr ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 ≠ ∅ )
70 elsni ( 𝑥 ∈ { 𝑧 } → 𝑥 = 𝑧 )
71 70 3ad2ant2 ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑥 = 𝑧 )
72 simp1 ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑧 = ∅ )
73 71 72 eqtrd ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑥 = ∅ )
74 simp3 ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑥 ≠ ∅ )
75 73 74 pm2.21ddne ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
76 67 68 69 75 syl3anc ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
77 simplr ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) )
78 elun ( 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑥𝑦𝑥 ∈ { 𝑧 } ) )
79 77 78 sylib ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥𝑦𝑥 ∈ { 𝑧 } ) )
80 65 76 79 mpjaodan ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
81 80 ex ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) )
82 81 ex ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ( 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
83 41 82 ralrimi ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧𝑦 ) ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) )
84 37 30 38 83 syl21anc ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) )
85 36 84 jca ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
86 85 ex ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) → ( ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
87 86 eximdv ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
88 vex 𝑓 ∈ V
89 snex { ⟨ 𝑧 , 𝑤 ⟩ } ∈ V
90 88 89 unex ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ∈ V
91 fneq1 ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) → ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ) )
92 fveq1 ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) → ( 𝑔𝑥 ) = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) )
93 92 eleq1d ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) → ( ( 𝑔𝑥 ) ∈ 𝑥 ↔ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) )
94 93 imbi2d ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) → ( ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ↔ ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
95 94 ralbidv ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
96 91 95 anbi12d ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) → ( ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ↔ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
97 90 96 spcev ( ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
98 97 eximi ( ∃ 𝑓 ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
99 87 98 syl6 ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ) )
100 ax5e ( ∃ 𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
101 99 100 syl6 ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ) )
102 101 imp ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ 𝑧 = ∅ ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
103 102 an32s ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ 𝑧 = ∅ ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
104 fneq1 ( 𝑓 = 𝑔 → ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ) )
105 fveq1 ( 𝑓 = 𝑔 → ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
106 105 eleq1d ( 𝑓 = 𝑔 → ( ( 𝑓𝑥 ) ∈ 𝑥 ↔ ( 𝑔𝑥 ) ∈ 𝑥 ) )
107 106 imbi2d ( 𝑓 = 𝑔 → ( ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
108 107 ralbidv ( 𝑓 = 𝑔 → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
109 104 108 anbi12d ( 𝑓 = 𝑔 → ( ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ) )
110 109 cbvexvw ( ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
111 103 110 sylibr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ 𝑧 = ∅ ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
112 simpllr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ¬ 𝑧𝑦 )
113 simpr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ¬ 𝑧 = ∅ )
114 neq0 ( ¬ 𝑧 = ∅ ↔ ∃ 𝑤 𝑤𝑧 )
115 113 114 sylib ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ∃ 𝑤 𝑤𝑧 )
116 simplr ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
117 115 116 jca ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
118 112 117 jca ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ( ¬ 𝑧𝑦 ∧ ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) )
119 exdistrv ( ∃ 𝑤𝑓 ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ↔ ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
120 simprrl ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑓 Fn 𝑦 )
121 120 25 sylib ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑓 : 𝑦 ⟶ V )
122 28 a1i ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑧 ∈ V )
123 simpl ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ¬ 𝑧𝑦 )
124 31 a1i ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑤 ∈ V )
125 121 122 123 124 33 syl121anc ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V )
126 125 35 sylibr ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) )
127 nfv 𝑥 ¬ 𝑧𝑦
128 nfv 𝑥 𝑤𝑧
129 nfv 𝑥 𝑓 Fn 𝑦
130 129 40 nfan 𝑥 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
131 128 130 nfan 𝑥 ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
132 127 131 nfan 𝑥 ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
133 simpr ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → 𝑥𝑦 )
134 simp-4l ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ¬ 𝑧𝑦 )
135 133 134 jca ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( 𝑥𝑦 ∧ ¬ 𝑧𝑦 ) )
136 48 50 syl ( ( 𝑥𝑦 ∧ ¬ 𝑧𝑦 ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = ( 𝑓𝑥 ) )
137 135 136 syl ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = ( 𝑓𝑥 ) )
138 simprrr ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
139 138 ad5ant12 ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) )
140 simplr ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → 𝑥 ≠ ∅ )
141 133 139 140 63 syl3c ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( 𝑓𝑥 ) ∈ 𝑥 )
142 137 141 eqeltrd ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥𝑦 ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
143 simplrl ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑤𝑧 )
144 143 adantr ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑤𝑧 )
145 144 adantr ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑤𝑧 )
146 simpr ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 ∈ { 𝑧 } )
147 146 70 syl ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 = 𝑧 )
148 fveq2 ( 𝑥 = 𝑧 → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑧 ) )
149 147 148 syl ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑧 ) )
150 28 a1i ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑧 ∈ V )
151 31 a1i ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑤 ∈ V )
152 simp-4l ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ¬ 𝑧𝑦 )
153 120 ad5ant12 ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑓 Fn 𝑦 )
154 153 fndmd ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → dom 𝑓 = 𝑦 )
155 152 154 neleqtrrd ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ dom 𝑓 )
156 fsnunfv ( ( 𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓 ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑧 ) = 𝑤 )
157 150 151 155 156 syl3anc ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑧 ) = 𝑤 )
158 149 157 eqtrd ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) = 𝑤 )
159 145 158 147 3eltr4d ( ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
160 simplr ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) )
161 160 78 sylib ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥𝑦𝑥 ∈ { 𝑧 } ) )
162 142 159 161 mpjaodan ( ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 )
163 162 ex ( ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) )
164 163 ex ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ( 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
165 132 164 ralrimi ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) )
166 126 165 jca ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑤 ⟩ } ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
167 166 97 syl ( ( ¬ 𝑧𝑦 ∧ ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
168 167 ex ( ¬ 𝑧𝑦 → ( ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ) )
169 168 2eximdv ( ¬ 𝑧𝑦 → ( ∃ 𝑤𝑓 ( 𝑤𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑤𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ) )
170 119 169 syl5bir ( ¬ 𝑧𝑦 → ( ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑤𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ) )
171 170 imp ( ( ¬ 𝑧𝑦 ∧ ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑤𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
172 100 exlimiv ( ∃ 𝑤𝑓𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
173 171 172 syl ( ( ¬ 𝑧𝑦 ∧ ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
174 173 110 sylibr ( ( ¬ 𝑧𝑦 ∧ ( ∃ 𝑤 𝑤𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
175 118 174 syl ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
176 111 175 pm2.61dan ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )
177 176 ex ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥𝑦 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) ) )
178 4 8 12 16 24 177 findcard2s ( 𝐴 ∈ Fin → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑓𝑥 ) ∈ 𝑥 ) ) )