Theorem fnchoice 44363

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 6640	. . . 4 ⊢ (𝑤 = ∅ → (𝑓 Fn 𝑤 ↔ 𝑓 Fn ∅))
2		raleq 3317	. . . 4 ⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
3	1, 2	anbi12d 630	. . 3 ⊢ (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
4	3	exbidv 1917	. 2 ⊢ (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
5		fneq2 6640	. . . 4 ⊢ (𝑤 = 𝑦 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝑦))
6		raleq 3317	. . . 4 ⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
7	5, 6	anbi12d 630	. . 3 ⊢ (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
8	7	exbidv 1917	. 2 ⊢ (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
9		fneq2 6640	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤 ↔ 𝑓 Fn (𝑦 ∪ {𝑧})))
10		raleq 3317	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
11	9, 10	anbi12d 630	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
12	11	exbidv 1917	. 2 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
13		fneq2 6640	. . . 4 ⊢ (𝑤 = 𝐴 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝐴))
14		raleq 3317	. . . 4 ⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
15	13, 14	anbi12d 630	. . 3 ⊢ (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
16	15	exbidv 1917	. 2 ⊢ (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
17		0ex 5301	. . . 4 ⊢ ∅ ∈ V
18		fneq1 6639	. . . 4 ⊢ (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19		eqid 2727	. . . . 5 ⊢ ∅ = ∅
20		fn0 6680	. . . . 5 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
21	19, 20	mpbir 230	. . . 4 ⊢ ∅ Fn ∅
22	17, 18, 21	ceqsexv2d 3524	. . 3 ⊢ ∃𝑓 𝑓 Fn ∅
23		ral0 4508	. . 3 ⊢ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
24	22, 23	exan 1858	. 2 ⊢ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
25		dffn2 6718	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑦 ↔ 𝑓:𝑦⟶V)
26	25	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → 𝑓:𝑦⟶V)
27	26	ad2antrl 727	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28		vex 3473	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ¬ 𝑧 ∈ 𝑦)
31		vex 3473	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33		fsnunf 7188	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
34	27, 29, 30, 32, 33	syl121anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35		dffn2 6718	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
36	34, 35	sylibr 233	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38		simprr 772	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
39		nfv 1910	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦)
40		nfra1 3276	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
41	39, 40	nfan 1895	. . . . . . . . . . . . . 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 3035	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑥 ≠ 𝑧)
48	47	necomd 2991	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑧 ≠ 𝑥)
49	46, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑧 ≠ 𝑥)
50		fvunsn 7182	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
52		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
53	52	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
54		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
55		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑥 → (𝑓‘𝑢) = (𝑓‘𝑥))
57	56	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑢))
58		eleq2w 2812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑥) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
59	57, 58	bitrd 279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
60	55, 59	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
61	60	cbvralvw 3229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
62	60	rspcv 3603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑦 → (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
63	61, 62	biimtrrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
64	42, 53, 54, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
65	51, 64	eqeltrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66		simp-4l 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
67	66	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70		elsni 4641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71	70	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72		simp1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
73	71, 72	eqtrd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74		simp3 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
75	73, 74	pm2.21ddne 3021	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
76	67, 68, 69, 75	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78		elun 4144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
79	77, 78	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
80	65, 76, 79	mpjaodan 957	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
81	80	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
82	81	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
83	41, 82	ralrimi 3249	. . . . . . . . . . . . 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 1913	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88		vex 3473	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
89		snex 5427	. . . . . . . . . . . 12 ⊢ {⟨𝑧, 𝑤⟩} ∈ V
90	88, 89	unex 7742	. . . . . . . . . . 11 ⊢ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91		fneq1 6639	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92		fveq1 6890	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
93	92	eleq1d 2813	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔‘𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
94	93	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
95	94	ralbidv 3172	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
96	91, 95	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
97	90, 96	spcev 3591	. . . . . . . . . 10 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
98	97	eximi 1830	. . . . . . . . 9 ⊢ (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
99	87, 98	syl6 35	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
100		ax5e 1908	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
101	99, 100	syl6 35	. . . . . . 7 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
102	101	imp 406	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
103	102	an32s 651	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
104		fneq1 6639	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105		fveq1 6890	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
106	105	eleq1d 2813	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑥) ∈ 𝑥))
107	106	imbi2d 340	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
108	107	ralbidv 3172	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
109	104, 108	anbi12d 630	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
110	109	cbvexvw 2033	. . . . 5 ⊢ (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
111	103, 110	sylibr 233	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
112		simpllr 775	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 ∈ 𝑦)
113		simpr 484	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114		neq0 4341	. . . . . . . 8 ⊢ (¬ 𝑧 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑧)
115	113, 114	sylib 217	. . . . . . 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 1952	. . . . . . . . 9 ⊢ (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
120		simprrl 780	. . . . . . . . . . . . . . . 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 1910	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ¬ 𝑧 ∈ 𝑦
128		nfv 1910	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
129		nfv 1910	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑓 Fn 𝑦
130	129, 40	nfan 1895	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
131	128, 130	nfan 1895	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
132	127, 131	nfan 1895	. . . . . . . . . . . . . 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	ad5ant12 755	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
140		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
141	133, 139, 140, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
142	137, 141	eqeltrd 2828	. . . . . . . . . . . . . . . . 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 6891	. . . . . . . . . . . . . . . . . . . 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	ad5ant12 755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154	153	fndmd 6653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155	152, 154	neleqtrrd 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156		fsnunfv 7190	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157	150, 151, 155, 156	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158	149, 157	eqtrd 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159	145, 158, 147	3eltr4d 2843	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161	160, 78	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
162	142, 159, 161	mpjaodan 957	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163	162	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164	163	ex 412	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165	132, 164	ralrimi 3249	. . . . . . . . . . . . 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 1915	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
170	119, 169	biimtrrid 242	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
171	170	imp 406	. . . . . . 7 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
172	100	exlimiv 1926	. . . . . . 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 812	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
177	176	ex 412	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
178	4, 8, 12, 16, 24, 177	findcard2s 9183	1 ⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846   ∧ w3a 1085   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2935  ∀wral 3056  Vcvv 3469   ∪ cun 3942  ∅c0 4318  {csn 4624  ⟨cop 4630  dom cdm 5672   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  Fincfn 8957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-om 7865  df-en 8958  df-fin 8961

This theorem is referenced by:  choicefi  44545  stoweidlem31  45391  stoweidlem35  45395  stoweidlem59  45419