Theorem fnchoice 42811

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 6563	. . . 4 ⊢ (𝑤 = ∅ → (𝑓 Fn 𝑤 ↔ 𝑓 Fn ∅))
2		raleq 3305	. . . 4 ⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
4	3	exbidv 1923	. 2 ⊢ (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
5		fneq2 6563	. . . 4 ⊢ (𝑤 = 𝑦 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝑦))
6		raleq 3305	. . . 4 ⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
7	5, 6	anbi12d 631	. . 3 ⊢ (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
8	7	exbidv 1923	. 2 ⊢ (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
9		fneq2 6563	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤 ↔ 𝑓 Fn (𝑦 ∪ {𝑧})))
10		raleq 3305	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
11	9, 10	anbi12d 631	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
12	11	exbidv 1923	. 2 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
13		fneq2 6563	. . . 4 ⊢ (𝑤 = 𝐴 → (𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝐴))
14		raleq 3305	. . . 4 ⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
15	13, 14	anbi12d 631	. . 3 ⊢ (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
16	15	exbidv 1923	. 2 ⊢ (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥 ∈ 𝑤 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
17		0ex 5245	. . . 4 ⊢ ∅ ∈ V
18		fneq1 6562	. . . 4 ⊢ (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19		eqid 2736	. . . . 5 ⊢ ∅ = ∅
20		fn0 6601	. . . . 5 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
21	19, 20	mpbir 230	. . . 4 ⊢ ∅ Fn ∅
22	17, 18, 21	ceqsexv2d 3489	. . 3 ⊢ ∃𝑓 𝑓 Fn ∅
23		ral0 4454	. . 3 ⊢ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
24	22, 23	exan 1864	. 2 ⊢ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
25		dffn2 6639	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑦 ↔ 𝑓:𝑦⟶V)
26	25	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑦 → 𝑓:𝑦⟶V)
27	26	ad2antrl 725	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30		simpllr 773	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ¬ 𝑧 ∈ 𝑦)
31		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑤 ∈ V
32	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33		fsnunf 7096	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
34	27, 29, 30, 32, 33	syl121anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35		dffn2 6639	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
36	34, 35	sylibr 233	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37		simplr 766	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38		simprr 770	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
39		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦)
40		nfra1 3263	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)
41	39, 40	nfan 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
42		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
43		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧 ∈ 𝑦)
44	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧 ∈ 𝑦)
45	44	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
46	42, 45	jca 512	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
47		nelne2 3039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑥 ≠ 𝑧)
48	47	necomd 2996	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → 𝑧 ≠ 𝑥)
49	46, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑧 ≠ 𝑥)
50		fvunsn 7090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
52		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
53	52	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
54		simplr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
55		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56		fveq2 6811	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = 𝑥 → (𝑓‘𝑢) = (𝑓‘𝑥))
57	56	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑢))
58		eleq2w 2820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑥) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
59	57, 58	bitrd 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑥 → ((𝑓‘𝑢) ∈ 𝑢 ↔ (𝑓‘𝑥) ∈ 𝑥))
60	55, 59	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
61	60	cbvralvw 3221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) ↔ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
62	60	rspcv 3565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑦 → (∀𝑢 ∈ 𝑦 (𝑢 ≠ ∅ → (𝑓‘𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
63	61, 62	syl5bir 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
64	42, 53, 54, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
65	51, 64	eqeltrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66		simp-4l 780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
67	66	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70		elsni 4587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71	70	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72		simp1 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
73	71, 72	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74		simp3 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
75	73, 74	pm2.21ddne 3026	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
76	67, 68, 69, 75	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78		elun 4093	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
79	77, 78	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
80	65, 76, 79	mpjaodan 956	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
81	80	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
82	81	ex 413	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
83	41, 82	ralrimi 3236	. . . . . . . . . . . . 13 ⊢ (((𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
84	37, 30, 38, 83	syl21anc 835	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
85	36, 84	jca 512	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
86	85	ex 413	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
87	86	eximdv 1919	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
89		snex 5368	. . . . . . . . . . . 12 ⊢ {⟨𝑧, 𝑤⟩} ∈ V
90	88, 89	unex 7637	. . . . . . . . . . 11 ⊢ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91		fneq1 6562	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92		fveq1 6810	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
93	92	eleq1d 2821	. . . . . . . . . . . . . 14 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔‘𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
94	93	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
95	94	ralbidv 3170	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
96	91, 95	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
97	90, 96	spcev 3553	. . . . . . . . . 10 ⊢ (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
98	97	eximi 1836	. . . . . . . . 9 ⊢ (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
99	87, 98	syl6 35	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
100		ax5e 1914	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
101	99, 100	syl6 35	. . . . . . 7 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
102	101	imp 407	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
103	102	an32s 649	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
104		fneq1 6562	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105		fveq1 6810	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥))
106	105	eleq1d 2821	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑥) ∈ 𝑥))
107	106	imbi2d 340	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
108	107	ralbidv 3170	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
109	104, 108	anbi12d 631	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
110	109	cbvexvw 2039	. . . . 5 ⊢ (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
111	103, 110	sylibr 233	. . . 4 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
112		simpllr 773	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 ∈ 𝑦)
113		simpr 485	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114		neq0 4289	. . . . . . . 8 ⊢ (¬ 𝑧 = ∅ ↔ ∃𝑤 𝑤 ∈ 𝑧)
115	113, 114	sylib 217	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤 ∈ 𝑧)
116		simplr 766	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
117	115, 116	jca 512	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
118	112, 117	jca 512	. . . . 5 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))))
119		exdistrv 1958	. . . . . . . . 9 ⊢ (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
120		simprrl 778	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121	120, 25	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
122	28	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
123		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ¬ 𝑧 ∈ 𝑦)
124	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
125	121, 122, 123, 124, 33	syl121anc 1374	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126	125, 35	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 ¬ 𝑧 ∈ 𝑦
128		nfv 1916	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧
129		nfv 1916	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑓 Fn 𝑦
130	129, 40	nfan 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
131	128, 130	nfan 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
132	127, 131	nfan 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
133		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑦)
134		simp-4l 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑦)
135	133, 134	jca 512	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦))
136	48, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓‘𝑥))
138		simprrr 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
139	138	ad5ant12 753	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))
140		simplr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → 𝑥 ≠ ∅)
141	133, 139, 140, 63	syl3c 66	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → (𝑓‘𝑥) ∈ 𝑥)
142	137, 141	eqeltrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ 𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143		simplrl 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤 ∈ 𝑧)
144	143	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤 ∈ 𝑧)
145	144	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ 𝑧)
146		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
147	146, 70	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
148		fveq2 6811	. . . . . . . . . . . . . . . . . . . 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 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑦)
153	120	ad5ant12 753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154	153	fndmd 6576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155	152, 154	neleqtrrd 2859	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156		fsnunfv 7098	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157	150, 151, 155, 156	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158	149, 157	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159	145, 158, 147	3eltr4d 2852	. . . . . . . . . . . . . . . . 17 ⊢ (((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161	160, 78	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥 ∈ 𝑦 ∨ 𝑥 ∈ {𝑧}))
162	142, 159, 161	mpjaodan 956	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163	162	ex 413	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164	163	ex 413	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165	132, 164	ralrimi 3236	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
166	126, 165	jca 512	. . . . . . . . . . . 12 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
167	166, 97	syl 17	. . . . . . . . . . 11 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
168	167	ex 413	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
169	168	2eximdv 1921	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → (∃𝑤∃𝑓(𝑤 ∈ 𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
170	119, 169	syl5bir 242	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))))
171	170	imp 407	. . . . . . 7 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (∃𝑤 𝑤 ∈ 𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))) → ∃𝑤∃𝑓∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
172	100	exlimiv 1932	. . . . . . 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 810	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
177	176	ex 413	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥 ∈ 𝑦 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥))))
178	4, 8, 12, 16, 24, 177	findcard2s 9008	1 ⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1540  ∃wex 1780   ∈ wcel 2105   ≠ wne 2940  ∀wral 3061  Vcvv 3440   ∪ cun 3894  ∅c0 4266  {csn 4570  ⟨cop 4576  dom cdm 5607   Fn wfn 6460  ⟶wf 6461  ‘cfv 6465  Fincfn 8782

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366  ax-un 7629

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-om 7759  df-en 8783  df-fin 8786

This theorem is referenced by:  choicefi  42986  stoweidlem31  43827  stoweidlem35  43831  stoweidlem59  43855