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 biimtrrid ⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
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 biimtrrid ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )