Theorem fnchoice 46320

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 6661	. . . 4 ⊢ (𝑤 = ∅ → (𝑓 Fn 𝑤 ↔ 𝑓 Fn ∅))
2		raleq 3320	. . . 4 ⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
4	3	exbidv 1956	. 2 ⊢ (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
5		fneq2 6661	. . . 4 ⊢ (𝑤 = 𝑦 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝑦))
6		raleq 3320	. . . 4 ⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
7	5, 6	anbi12d 644	. . 3 ⊢ (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
8	7	exbidv 1956	. 2 ⊢ (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
9		fneq2 6661	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤 ↔ 𝑓 Fn (𝑦 ∪ {𝑧})))
10		raleq 3320	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
11	9, 10	anbi12d 644	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
12	11	exbidv 1956	. 2 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
13		fneq2 6661	. . . 4 ⊢ (𝑤 = 𝐴 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝐴))
14		raleq 3320	. . . 4 ⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
15	13, 14	anbi12d 644	. . 3 ⊢ (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
16	15	exbidv 1956	. 2 ⊢ (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
17		0ex 5267	. . . 4 ⊢ ∅ ∈ V
18		fneq1 6660	. . . 4 ⊢ (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19		eqid 2763	. . . . 5 ⊢ ∅ = ∅
20		fn0 6700	. . . . 5 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
21	19, 20	mpbir 234	. . . 4 ⊢ ∅ Fn ∅
22	17, 18, 21	ceqsexv2d 3503	. . 3 ⊢ ∃𝑓 𝑓 Fn ∅
23		ral0 4457	. . 3 ⊢ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
24	22, 23	exan 1895	. 2 ⊢ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
25		dffn2 6741	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑦 ↔ 𝑓:𝑦⟶V)
26	25	biimpi 219	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → 𝑓:𝑦⟶V)
27	26	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30		simpllr 788	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ¬ 𝑧 ∈ 𝑦)
31		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33		fsnunf 7221	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
34	27, 29, 30, 32, 33	syl121anc 1403	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35		dffn2 6741	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
36	34, 35	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38		simprr 785	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
39		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦)
40		nfra1 3290	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
41	39, 40	nfan 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
42		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
43		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧 ∈ 𝑦)
44	43	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧 ∈ 𝑦)
45	44	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
46	42, 45	jca 521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
47		nelne2 3057	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑥 ≠ 𝑧)
48	47	necomd 3014	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑧 ≠ 𝑥)
49	46, 48	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑧 ≠ 𝑥)
50		fvunsn 7215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
51	49, 50	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
52		simpllr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
53	52	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
54		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
55		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑥 → (𝑓‘𝑢) = (𝑓‘𝑥))
57	56	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑢))
58		eleq2w 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑥) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
59	57, 58	bitrd 282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
60	55, 59	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
61	60	cbvralvw 3244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
62	60	rspcv 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑦 → (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
63	61, 62	biimtrrid 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
64	42, 53, 54, 63	syl3c 67	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
65	51, 64	eqeltrd 2864	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66		simp-4l 795	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
67	66	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70		elsni 4601	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71	70	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72		simp1 1154	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
73	71, 72	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74		simp3 1156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
75	73, 74	pm2.21ddne 3043	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
76	67, 68, 69, 75	syl3anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78		elun 4155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
79	77, 78	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
80	65, 76, 79	mpjaodan 973	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
81	80	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
82	81	ex 418	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
83	41, 82	ralrimi 3264	. . . . . . . . . . . . 13 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
84	37, 30, 38, 83	syl21anc 851	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
85	36, 84	jca 521	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
86	85	ex 418	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
87	86	eximdv 1952	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
89		snex 5404	. . . . . . . . . . . 12 ⊢ {⟨𝑧, 𝑤⟩} ∈ V
90	88, 89	unex 7793	. . . . . . . . . . 11 ⊢ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91		fneq1 6660	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92		fveq1 6915	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
93	92	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔‘𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
94	93	imbi2d 343	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
95	94	ralbidv 3189	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
96	91, 95	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
97	90, 96	spcev 3564	. . . . . . . . . 10 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
98	97	eximi 1868	. . . . . . . . 9 ⊢ (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
99	87, 98	syl6 36	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
100		ax5e 1947	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
101	99, 100	syl6 36	. . . . . . 7 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
102	101	imp 412	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
103	102	an32s 665	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
104		fneq1 6660	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105		fveq1 6915	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
106	105	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑥) ∈ 𝑥))
107	106	imbi2d 343	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
108	107	ralbidv 3189	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
109	104, 108	anbi12d 644	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
110	109	cbvexvw 2072	. . . . 5 ⊢ (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
111	103, 110	sylibr 237	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
112		simpllr 788	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 ∈ 𝑦)
113		simpr 490	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114		neq0 4302	. . . . . . . 8 ⊢ (¬ 𝑧 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑧)
115	113, 114	sylib 221	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤 ∈ 𝑧)
116		simplr 781	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
117	115, 116	jca 521	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
118	112, 117	jca 521	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))))
119		exdistrv 1990	. . . . . . . . 9 ⊢ (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
120		simprrl 793	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121	120, 25	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
122	28	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
123		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ¬ 𝑧 ∈ 𝑦)
124	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
125	121, 122, 123, 124, 33	syl121anc 1403	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126	125, 35	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ¬ 𝑧 ∈ 𝑦
128		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
129		nfv 1949	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑓 Fn 𝑦
130	129, 40	nfan 1934	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
131	128, 130	nfan 1934	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
132	127, 131	nfan 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
133		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
134		simp-4l 795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
135	133, 134	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
136	48, 50	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
137	135, 136	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
138		simprrr 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
139	138	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
140		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
141	133, 139, 140, 63	syl3c 67	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
142	137, 141	eqeltrd 2864	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143		simplrl 789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤 ∈ 𝑧)
144	143	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤 ∈ 𝑧)
145	144	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ 𝑧)
146		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
147	146, 70	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
148		fveq2 6916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
149	147, 148	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
150	28	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
151	31	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
152		simp-4l 795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑦)
153	120	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154	153	fndmd 6674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155	152, 154	neleqtrrd 2887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156		fsnunfv 7223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157	150, 151, 155, 156	syl3anc 1399	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158	149, 157	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159	145, 158, 147	3eltr4d 2879	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161	160, 78	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
162	142, 159, 161	mpjaodan 973	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163	162	ex 418	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164	163	ex 418	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165	132, 164	ralrimi 3264	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
166	126, 165	jca 521	. . . . . . . . . . . 12 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
167	166, 97	syl 18	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
168	167	ex 418	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
169	168	2eximdv 1954	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
170	119, 169	biimtrrid 246	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
171	170	imp 412	. . . . . . 7 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
172	100	exlimiv 1965	. . . . . . 7 ⊢ (∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
173	171, 172	syl 18	. . . . . 6 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
174	173, 110	sylibr 237	. . . . 5 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
175	118, 174	syl 18	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
176	111, 175	pm2.61dan 825	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
177	176	ex 418	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
178	4, 8, 12, 16, 24, 177	findcard2s 9219	1 ⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  Vcvv 3454   ∪ cun 4152  ∅c0 4281  {csn 4588  ⟨cop 4840  dom cdm 5658   Fn wfn 6561  ⟶wf 6562  ‘cfv 6566  Fincfn 9011

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-om 7912  df-en 9012  df-fin 9015

This theorem is used by:  choicefi  46487  stoweidlem31  47314  stoweidlem35  47318  stoweidlem59  47342