Theorem fnchoice 42461

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

Assertion

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

Distinct variable group:   𝑥,𝑓,𝐴

Proof of Theorem fnchoice

Dummy variables 𝑔 𝑤 𝑦 𝑧 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fneq2 6509	. . . 4 ⊢ (𝑤 = ∅ → (𝑓 Fn 𝑤 ↔ 𝑓 Fn ∅))
2		raleq 3333	. . . 4 ⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
3	1, 2	anbi12d 630	. . 3 ⊢ (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
4	3	exbidv 1925	. 2 ⊢ (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
5		fneq2 6509	. . . 4 ⊢ (𝑤 = 𝑦 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝑦))
6		raleq 3333	. . . 4 ⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
7	5, 6	anbi12d 630	. . 3 ⊢ (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
8	7	exbidv 1925	. 2 ⊢ (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
9		fneq2 6509	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤 ↔ 𝑓 Fn (𝑦 ∪ {𝑧})))
10		raleq 3333	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
11	9, 10	anbi12d 630	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
12	11	exbidv 1925	. 2 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
13		fneq2 6509	. . . 4 ⊢ (𝑤 = 𝐴 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝐴))
14		raleq 3333	. . . 4 ⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
15	13, 14	anbi12d 630	. . 3 ⊢ (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
16	15	exbidv 1925	. 2 ⊢ (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
17		0ex 5226	. . . 4 ⊢ ∅ ∈ V
18		fneq1 6508	. . . 4 ⊢ (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19		eqid 2738	. . . . 5 ⊢ ∅ = ∅
20		fn0 6548	. . . . 5 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
21	19, 20	mpbir 230	. . . 4 ⊢ ∅ Fn ∅
22	17, 18, 21	ceqsexv2d 3471	. . 3 ⊢ ∃𝑓 𝑓 Fn ∅
23		ral0 4440	. . 3 ⊢ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
24	22, 23	exan 1866	. 2 ⊢ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
25		dffn2 6586	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑦 ↔ 𝑓:𝑦⟶V)
26	25	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → 𝑓:𝑦⟶V)
27	26	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28		vex 3426	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30		simpllr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ¬ 𝑧 ∈ 𝑦)
31		vex 3426	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33		fsnunf 7039	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
34	27, 29, 30, 32, 33	syl121anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35		dffn2 6586	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
36	34, 35	sylibr 233	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37		simplr 765	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38		simprr 769	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
39		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦)
40		nfra1 3142	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
41	39, 40	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
42		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
43		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧 ∈ 𝑦)
44	43	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧 ∈ 𝑦)
45	44	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
46	42, 45	jca 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
47		nelne2 3041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑥 ≠ 𝑧)
48	47	necomd 2998	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑧 ≠ 𝑥)
49	46, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑧 ≠ 𝑥)
50		fvunsn 7033	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
52		simpllr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
53	52	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
54		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
55		neeq1 3005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑥 → (𝑓‘𝑢) = (𝑓‘𝑥))
57	56	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑢))
58		eleq2w 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑥) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
59	57, 58	bitrd 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
60	55, 59	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
61	60	cbvralvw 3372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
62	60	rspcv 3547	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑦 → (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
63	61, 62	syl5bir 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
64	42, 53, 54, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
65	51, 64	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66		simp-4l 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
67	66	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69		simplr 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70		elsni 4575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71	70	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72		simp1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
73	71, 72	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74		simp3 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
75	73, 74	pm2.21ddne 3028	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
76	67, 68, 69, 75	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77		simplr 765	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78		elun 4079	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
79	77, 78	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
80	65, 76, 79	mpjaodan 955	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
81	80	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
82	81	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
83	41, 82	ralrimi 3139	. . . . . . . . . . . . 13 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
84	37, 30, 38, 83	syl21anc 834	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
85	36, 84	jca 511	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
86	85	ex 412	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
87	86	eximdv 1921	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88		vex 3426	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
89		snex 5349	. . . . . . . . . . . 12 ⊢ {⟨𝑧, 𝑤⟩} ∈ V
90	88, 89	unex 7574	. . . . . . . . . . 11 ⊢ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91		fneq1 6508	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92		fveq1 6755	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
93	92	eleq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔‘𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
94	93	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
95	94	ralbidv 3120	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
96	91, 95	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
97	90, 96	spcev 3535	. . . . . . . . . 10 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
98	97	eximi 1838	. . . . . . . . 9 ⊢ (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
99	87, 98	syl6 35	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
100		ax5e 1916	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
101	99, 100	syl6 35	. . . . . . 7 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
102	101	imp 406	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
103	102	an32s 648	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
104		fneq1 6508	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105		fveq1 6755	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
106	105	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑥) ∈ 𝑥))
107	106	imbi2d 340	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
108	107	ralbidv 3120	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
109	104, 108	anbi12d 630	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
110	109	cbvexvw 2041	. . . . 5 ⊢ (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
111	103, 110	sylibr 233	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
112		simpllr 772	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 ∈ 𝑦)
113		simpr 484	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114		neq0 4276	. . . . . . . 8 ⊢ (¬ 𝑧 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑧)
115	113, 114	sylib 217	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤 ∈ 𝑧)
116		simplr 765	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
117	115, 116	jca 511	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
118	112, 117	jca 511	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))))
119		exdistrv 1960	. . . . . . . . 9 ⊢ (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
120		simprrl 777	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121	120, 25	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
122	28	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
123		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ¬ 𝑧 ∈ 𝑦)
124	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
125	121, 122, 123, 124, 33	syl121anc 1373	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126	125, 35	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ¬ 𝑧 ∈ 𝑦
128		nfv 1918	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
129		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑓 Fn 𝑦
130	129, 40	nfan 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
131	128, 130	nfan 1903	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
132	127, 131	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
133		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
134		simp-4l 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
135	133, 134	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
136	48, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
138		simprrr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
139	138	ad5ant12 752	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
140		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
141	133, 139, 140, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
142	137, 141	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143		simplrl 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤 ∈ 𝑧)
144	143	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤 ∈ 𝑧)
145	144	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ 𝑧)
146		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
147	146, 70	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
148		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
149	147, 148	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
150	28	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
151	31	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
152		simp-4l 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑦)
153	120	ad5ant12 752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154	153	fndmd 6522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155	152, 154	neleqtrrd 2861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156		fsnunfv 7041	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157	150, 151, 155, 156	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158	149, 157	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159	145, 158, 147	3eltr4d 2854	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160		simplr 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161	160, 78	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
162	142, 159, 161	mpjaodan 955	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163	162	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164	163	ex 412	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165	132, 164	ralrimi 3139	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
166	126, 165	jca 511	. . . . . . . . . . . 12 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
167	166, 97	syl 17	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
168	167	ex 412	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
169	168	2eximdv 1923	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
170	119, 169	syl5bir 242	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
171	170	imp 406	. . . . . . 7 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
172	100	exlimiv 1934	. . . . . . 7 ⊢ (∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
173	171, 172	syl 17	. . . . . 6 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
174	173, 110	sylibr 233	. . . . 5 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
175	118, 174	syl 17	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
176	111, 175	pm2.61dan 809	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
177	176	ex 412	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
178	4, 8, 12, 16, 24, 177	findcard2s 8910	1 ⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  Vcvv 3422   ∪ cun 3881  ∅c0 4253  {csn 4558  ⟨cop 4564  dom cdm 5580   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  Fincfn 8691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-en 8692  df-fin 8695

This theorem is referenced by:  choicefi  42629  stoweidlem31  43462  stoweidlem35  43466  stoweidlem59  43490