Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnchoice Structured version   Visualization version   GIF version

Theorem fnchoice 38706
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.
StepHypRef Expression
1 fneq2 5943 . . . 4 (𝑤 = ∅ → (𝑓 Fn 𝑤𝑓 Fn ∅))
2 raleq 3130 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
31, 2anbi12d 746 . . 3 (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
43exbidv 1847 . 2 (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
5 fneq2 5943 . . . 4 (𝑤 = 𝑦 → (𝑓 Fn 𝑤𝑓 Fn 𝑦))
6 raleq 3130 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
75, 6anbi12d 746 . . 3 (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
87exbidv 1847 . 2 (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
9 fneq2 5943 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤𝑓 Fn (𝑦 ∪ {𝑧})))
10 raleq 3130 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119, 10anbi12d 746 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1211exbidv 1847 . 2 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
13 fneq2 5943 . . . 4 (𝑤 = 𝐴 → (𝑓 Fn 𝑤𝑓 Fn 𝐴))
14 raleq 3130 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
1513, 14anbi12d 746 . . 3 (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1615exbidv 1847 . 2 (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
17 eqid 2621 . . . . . 6 ∅ = ∅
18 fn0 5973 . . . . . 6 (∅ Fn ∅ ↔ ∅ = ∅)
1917, 18mpbir 221 . . . . 5 ∅ Fn ∅
20 0ex 4755 . . . . . 6 ∅ ∈ V
21 fneq1 5942 . . . . . 6 (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
2220, 21spcev 3289 . . . . 5 (∅ Fn ∅ → ∃𝑓 𝑓 Fn ∅)
2319, 22ax-mp 5 . . . 4 𝑓 𝑓 Fn ∅
24 ral0 4053 . . . 4 𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
2523, 24pm3.2i 471 . . 3 (∃𝑓 𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
2625exan 1785 . 2 𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
27 dffn2 6009 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2827biimpi 206 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2928ad2antrl 763 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
30 vex 3192 . . . . . . . . . . . . . . 15 𝑧 ∈ V
3130a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
32 simpllr 798 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ¬ 𝑧𝑦)
33 vex 3192 . . . . . . . . . . . . . . 15 𝑤 ∈ V
3433a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
35 fsnunf 6411 . . . . . . . . . . . . . 14 ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3629, 31, 32, 34, 35syl121anc 1328 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
37 dffn2 6009 . . . . . . . . . . . . 13 ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3836, 37sylibr 224 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
39 simplr 791 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 = ∅)
40 simprr 795 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
41 nfv 1840 . . . . . . . . . . . . . . 15 𝑥(𝑧 = ∅ ∧ ¬ 𝑧𝑦)
42 nfra1 2936 . . . . . . . . . . . . . . 15 𝑥𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
4341, 42nfan 1825 . . . . . . . . . . . . . 14 𝑥((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
44 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
45 simpllr 798 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧𝑦)
4645adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧𝑦)
4746adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
4844, 47jca 554 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
49 nelne2 2887 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑥𝑧)
5049necomd 2845 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑥)
5148, 50syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑧𝑥)
52 fvunsn 6405 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
5351, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
54 simpllr 798 . . . . . . . . . . . . . . . . . . . 20 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
5554adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
56 simplr 791 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
57 neeq1 2852 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
58 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑥 → (𝑓𝑢) = (𝑓𝑥))
5958eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑢))
60 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑥) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6159, 60bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6257, 61imbi12d 334 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6362cbvralv 3162 . . . . . . . . . . . . . . . . . . . 20 (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
6462rspcv 3294 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6563, 64syl5bir 233 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 → (∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6644, 55, 56, 65syl3c 66 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
6753, 66eqeltrd 2698 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
68 simp-4l 805 . . . . . . . . . . . . . . . . . . 19 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
6968adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
70 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
71 simplr 791 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
72 elsni 4170 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
73723ad2ant2 1081 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
74 simp1 1059 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
7573, 74eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
76 simp3 1061 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
7775, 76pm2.21ddne 2874 . . . . . . . . . . . . . . . . . 18 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
7869, 70, 71, 77syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
79 simplr 791 . . . . . . . . . . . . . . . . . 18 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
80 elun 3736 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥𝑦𝑥 ∈ {𝑧}))
8179, 80sylib 208 . . . . . . . . . . . . . . . . 17 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
8267, 78, 81mpjaodan 826 . . . . . . . . . . . . . . . 16 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
8382ex 450 . . . . . . . . . . . . . . 15 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8483ex 450 . . . . . . . . . . . . . 14 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8543, 84ralrimi 2952 . . . . . . . . . . . . 13 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8639, 32, 40, 85syl21anc 1322 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8738, 86jca 554 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8887ex 450 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
8988eximdv 1843 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
90 vex 3192 . . . . . . . . . . . 12 𝑓 ∈ V
91 snex 4874 . . . . . . . . . . . 12 {⟨𝑧, 𝑤⟩} ∈ V
9290, 91unex 6916 . . . . . . . . . . 11 (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
93 fneq1 5942 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
94 fveq1 6152 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
9594eleq1d 2683 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
9695imbi2d 330 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9796ralbidv 2981 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9893, 97anbi12d 746 . . . . . . . . . . 11 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
9992, 98spcev 3289 . . . . . . . . . 10 (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10099eximi 1759 . . . . . . . . 9 (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10189, 100syl6 35 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
102 ax5e 1838 . . . . . . . 8 (∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
103101, 102syl6 35 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
104103imp 445 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
105104an32s 845 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
106 fneq1 5942 . . . . . . 7 (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
107 fveq1 6152 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
108107eleq1d 2683 . . . . . . . . 9 (𝑓 = 𝑔 → ((𝑓𝑥) ∈ 𝑥 ↔ (𝑔𝑥) ∈ 𝑥))
109108imbi2d 330 . . . . . . . 8 (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
110109ralbidv 2981 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
111106, 110anbi12d 746 . . . . . 6 (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
112111cbvexv 2274 . . . . 5 (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
113105, 112sylibr 224 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
114 simpllr 798 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧𝑦)
115 simpr 477 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
116 neq0 3911 . . . . . . . 8 𝑧 = ∅ ↔ ∃𝑤 𝑤𝑧)
117115, 116sylib 208 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤𝑧)
118 simplr 791 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119117, 118jca 554 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
120114, 119jca 554 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))))
121 eeanv 2181 . . . . . . . . 9 (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
122 simprrl 803 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
123122, 27sylib 208 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
12430a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
125 simpl 473 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ¬ 𝑧𝑦)
12633a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
127123, 124, 125, 126, 35syl121anc 1328 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
128127, 37sylibr 224 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
129 nfv 1840 . . . . . . . . . . . . . . 15 𝑥 ¬ 𝑧𝑦
130 nfv 1840 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝑧
131 nfv 1840 . . . . . . . . . . . . . . . . 17 𝑥 𝑓 Fn 𝑦
132131, 42nfan 1825 . . . . . . . . . . . . . . . 16 𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
133130, 132nfan 1825 . . . . . . . . . . . . . . 15 𝑥(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
134129, 133nfan 1825 . . . . . . . . . . . . . 14 𝑥𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
135 simpr 477 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
136 simp-4l 805 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
137135, 136jca 554 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
13850, 52syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
139137, 138syl 17 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
140 simprrr 804 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
141140adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
142141adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
143142adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
144 simplr 791 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
145135, 143, 144, 65syl3c 66 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
146139, 145eqeltrd 2698 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
147 simplrl 799 . . . . . . . . . . . . . . . . . . . 20 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤𝑧)
148147adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤𝑧)
149148adantr 481 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤𝑧)
150 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
151150, 72syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
152 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
15430a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
15533a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
156 simp-4l 805 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧𝑦)
157122adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑓 Fn 𝑦)
158157adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑓 Fn 𝑦)
159158adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
160 fndm 5953 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 Fn 𝑦 → dom 𝑓 = 𝑦)
161159, 160syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
162156, 161neleqtrrd 2720 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
163 fsnunfv 6413 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
164154, 155, 162, 163syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
165153, 164eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
166149, 165, 1513eltr4d 2713 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
167 simplr 791 . . . . . . . . . . . . . . . . . 18 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
168167, 80sylib 208 . . . . . . . . . . . . . . . . 17 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
169146, 166, 168mpjaodan 826 . . . . . . . . . . . . . . . 16 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
170169ex 450 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
171170ex 450 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
172134, 171ralrimi 2952 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
173128, 172jca 554 . . . . . . . . . . . 12 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
174173, 99syl 17 . . . . . . . . . . 11 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
175174ex 450 . . . . . . . . . 10 𝑧𝑦 → ((𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
1761752eximdv 1845 . . . . . . . . 9 𝑧𝑦 → (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
177121, 176syl5bir 233 . . . . . . . 8 𝑧𝑦 → ((∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
178177imp 445 . . . . . . 7 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
179102exlimiv 1855 . . . . . . 7 (∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
180178, 179syl 17 . . . . . 6 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
181180, 112sylibr 224 . . . . 5 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
182120, 181syl 17 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
183113, 182pm2.61dan 831 . . 3 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
184183ex 450 . 2 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1854, 8, 12, 16, 26, 184findcard2s 8153 1 (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  Vcvv 3189  cun 3557  c0 3896  {csn 4153  cop 4159  dom cdm 5079   Fn wfn 5847  wf 5848  cfv 5852  Fincfn 7907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-1o 7512  df-er 7694  df-en 7908  df-fin 7911
This theorem is referenced by:  choicefi  38897  stoweidlem31  39581  stoweidlem35  39585  stoweidlem59  39609
  Copyright terms: Public domain W3C validator