Theorem fnchoice 45274

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 6584	. . . 4 ⊢ (𝑤 = ∅ → (𝑓 Fn 𝑤 ↔ 𝑓 Fn ∅))
2		raleq 3293	. . . 4 ⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
4	3	exbidv 1922	. 2 ⊢ (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
5		fneq2 6584	. . . 4 ⊢ (𝑤 = 𝑦 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝑦))
6		raleq 3293	. . . 4 ⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
7	5, 6	anbi12d 632	. . 3 ⊢ (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
8	7	exbidv 1922	. 2 ⊢ (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
9		fneq2 6584	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤 ↔ 𝑓 Fn (𝑦 ∪ {𝑧})))
10		raleq 3293	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
11	9, 10	anbi12d 632	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
12	11	exbidv 1922	. 2 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
13		fneq2 6584	. . . 4 ⊢ (𝑤 = 𝐴 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝐴))
14		raleq 3293	. . . 4 ⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
15	13, 14	anbi12d 632	. . 3 ⊢ (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
16	15	exbidv 1922	. 2 ⊢ (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
17		0ex 5252	. . . 4 ⊢ ∅ ∈ V
18		fneq1 6583	. . . 4 ⊢ (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19		eqid 2736	. . . . 5 ⊢ ∅ = ∅
20		fn0 6623	. . . . 5 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
21	19, 20	mpbir 231	. . . 4 ⊢ ∅ Fn ∅
22	17, 18, 21	ceqsexv2d 3491	. . 3 ⊢ ∃𝑓 𝑓 Fn ∅
23		ral0 4451	. . 3 ⊢ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
24	22, 23	exan 1863	. 2 ⊢ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
25		dffn2 6664	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑦 ↔ 𝑓:𝑦⟶V)
26	25	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → 𝑓:𝑦⟶V)
27	26	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ¬ 𝑧 ∈ 𝑦)
31		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33		fsnunf 7131	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
34	27, 29, 30, 32, 33	syl121anc 1377	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35		dffn2 6664	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
36	34, 35	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38		simprr 772	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
39		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦)
40		nfra1 3260	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
41	39, 40	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
42		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
43		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧 ∈ 𝑦)
44	43	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧 ∈ 𝑦)
45	44	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
46	42, 45	jca 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
47		nelne2 3030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑥 ≠ 𝑧)
48	47	necomd 2987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑧 ≠ 𝑥)
49	46, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑧 ≠ 𝑥)
50		fvunsn 7125	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
52		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
53	52	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
54		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
55		neeq1 2994	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑥 → (𝑓‘𝑢) = (𝑓‘𝑥))
57	56	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑢))
58		eleq2w 2820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑥) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
59	57, 58	bitrd 279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
60	55, 59	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
61	60	cbvralvw 3214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
62	60	rspcv 3572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑦 → (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
63	61, 62	biimtrrid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
64	42, 53, 54, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
65	51, 64	eqeltrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66		simp-4l 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
67	66	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70		elsni 4597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71	70	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72		simp1 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
73	71, 72	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74		simp3 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
75	73, 74	pm2.21ddne 3016	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
76	67, 68, 69, 75	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78		elun 4105	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
79	77, 78	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
80	65, 76, 79	mpjaodan 960	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
81	80	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
82	81	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
83	41, 82	ralrimi 3234	. . . . . . . . . . . . 13 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
84	37, 30, 38, 83	syl21anc 837	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
85	36, 84	jca 511	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
86	85	ex 412	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
87	86	eximdv 1918	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
89		snex 5381	. . . . . . . . . . . 12 ⊢ {⟨𝑧, 𝑤⟩} ∈ V
90	88, 89	unex 7689	. . . . . . . . . . 11 ⊢ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91		fneq1 6583	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92		fveq1 6833	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
93	92	eleq1d 2821	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔‘𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
94	93	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
95	94	ralbidv 3159	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
96	91, 95	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
97	90, 96	spcev 3560	. . . . . . . . . 10 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
98	97	eximi 1836	. . . . . . . . 9 ⊢ (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
99	87, 98	syl6 35	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
100		ax5e 1913	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
101	99, 100	syl6 35	. . . . . . 7 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
102	101	imp 406	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
103	102	an32s 652	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
104		fneq1 6583	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105		fveq1 6833	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
106	105	eleq1d 2821	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑥) ∈ 𝑥))
107	106	imbi2d 340	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
108	107	ralbidv 3159	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
109	104, 108	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
110	109	cbvexvw 2038	. . . . 5 ⊢ (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
111	103, 110	sylibr 234	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
112		simpllr 775	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 ∈ 𝑦)
113		simpr 484	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114		neq0 4304	. . . . . . . 8 ⊢ (¬ 𝑧 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑧)
115	113, 114	sylib 218	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤 ∈ 𝑧)
116		simplr 768	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
117	115, 116	jca 511	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
118	112, 117	jca 511	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))))
119		exdistrv 1956	. . . . . . . . 9 ⊢ (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
120		simprrl 780	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121	120, 25	sylib 218	. . . . . . . . . . . . . . 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 1377	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126	125, 35	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ¬ 𝑧 ∈ 𝑦
128		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
129		nfv 1915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑓 Fn 𝑦
130	129, 40	nfan 1900	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
131	128, 130	nfan 1900	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
132	127, 131	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
133		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
134		simp-4l 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
135	133, 134	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
136	48, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
138		simprrr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
139	138	ad3antrrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
140		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
141	133, 139, 140, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
142	137, 141	eqeltrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143		simplrl 776	. . . . . . . . . . . . . . . . . . . 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 6834	. . . . . . . . . . . . . . . . . . . 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 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑦)
153	120	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154	153	fndmd 6597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155	152, 154	neleqtrrd 2859	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156		fsnunfv 7133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157	150, 151, 155, 156	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158	149, 157	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159	145, 158, 147	3eltr4d 2851	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161	160, 78	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
162	142, 159, 161	mpjaodan 960	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163	162	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164	163	ex 412	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165	132, 164	ralrimi 3234	. . . . . . . . . . . . 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 1920	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
170	119, 169	biimtrrid 243	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
171	170	imp 406	. . . . . . 7 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
172	100	exlimiv 1931	. . . . . . 7 ⊢ (∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
173	171, 172	syl 17	. . . . . 6 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
174	173, 110	sylibr 234	. . . . 5 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
175	118, 174	syl 17	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
176	111, 175	pm2.61dan 812	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
177	176	ex 412	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
178	4, 8, 12, 16, 24, 177	findcard2s 9090	1 ⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  Vcvv 3440   ∪ cun 3899  ∅c0 4285  {csn 4580  ⟨cop 4586  dom cdm 5624   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-om 7809  df-en 8884  df-fin 8887

This theorem is referenced by:  choicefi  45444  stoweidlem31  46275  stoweidlem35  46279  stoweidlem59  46303