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 39710
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 6120 . . . 4 (𝑤 = ∅ → (𝑓 Fn 𝑤𝑓 Fn ∅))
2 raleq 3287 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
31, 2anbi12d 608 . . 3 (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
43exbidv 2002 . 2 (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
5 fneq2 6120 . . . 4 (𝑤 = 𝑦 → (𝑓 Fn 𝑤𝑓 Fn 𝑦))
6 raleq 3287 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
75, 6anbi12d 608 . . 3 (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
87exbidv 2002 . 2 (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
9 fneq2 6120 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤𝑓 Fn (𝑦 ∪ {𝑧})))
10 raleq 3287 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119, 10anbi12d 608 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1211exbidv 2002 . 2 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
13 fneq2 6120 . . . 4 (𝑤 = 𝐴 → (𝑓 Fn 𝑤𝑓 Fn 𝐴))
14 raleq 3287 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
1513, 14anbi12d 608 . . 3 (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1615exbidv 2002 . 2 (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
17 eqid 2771 . . . . . 6 ∅ = ∅
18 fn0 6151 . . . . . 6 (∅ Fn ∅ ↔ ∅ = ∅)
1917, 18mpbir 221 . . . . 5 ∅ Fn ∅
20 0ex 4924 . . . . . 6 ∅ ∈ V
21 fneq1 6119 . . . . . 6 (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
2220, 21spcev 3451 . . . . 5 (∅ Fn ∅ → ∃𝑓 𝑓 Fn ∅)
2319, 22ax-mp 5 . . . 4 𝑓 𝑓 Fn ∅
24 ral0 4217 . . . 4 𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
2523, 24pm3.2i 447 . . 3 (∃𝑓 𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
2625exan 1939 . 2 𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
27 dffn2 6187 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2827biimpi 206 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2928ad2antrl 699 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
30 vex 3354 . . . . . . . . . . . . . . 15 𝑧 ∈ V
3130a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
32 simpllr 752 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ¬ 𝑧𝑦)
33 vex 3354 . . . . . . . . . . . . . . 15 𝑤 ∈ V
3433a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
35 fsnunf 6595 . . . . . . . . . . . . . 14 ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3629, 31, 32, 34, 35syl121anc 1481 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
37 dffn2 6187 . . . . . . . . . . . . 13 ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3836, 37sylibr 224 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
39 simplr 744 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 = ∅)
40 simprr 748 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
41 nfv 1995 . . . . . . . . . . . . . . 15 𝑥(𝑧 = ∅ ∧ ¬ 𝑧𝑦)
42 nfra1 3090 . . . . . . . . . . . . . . 15 𝑥𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
4341, 42nfan 1980 . . . . . . . . . . . . . 14 𝑥((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
44 simpr 471 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
45 simpllr 752 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧𝑦)
4645adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧𝑦)
4746adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
4844, 47jca 495 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
49 nelne2 3040 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑥𝑧)
5049necomd 2998 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑥)
5148, 50syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑧𝑥)
52 fvunsn 6589 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
5351, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
54 simpllr 752 . . . . . . . . . . . . . . . . . . . 20 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
5554adantr 466 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
56 simplr 744 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
57 neeq1 3005 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
58 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑥 → (𝑓𝑢) = (𝑓𝑥))
5958eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑢))
60 eleq2w 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑥) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6159, 60bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6257, 61imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6362cbvralv 3320 . . . . . . . . . . . . . . . . . . . 20 (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
6462rspcv 3456 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6563, 64syl5bir 233 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 → (∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6644, 55, 56, 65syl3c 66 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
6753, 66eqeltrd 2850 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
68 simp-4l 760 . . . . . . . . . . . . . . . . . . 19 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
6968adantr 466 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
70 simpr 471 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
71 simplr 744 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
72 elsni 4333 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
73723ad2ant2 1128 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
74 simp1 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
7573, 74eqtrd 2805 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
76 simp3 1132 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
7775, 76pm2.21ddne 3027 . . . . . . . . . . . . . . . . . 18 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
7869, 70, 71, 77syl3anc 1476 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
79 simplr 744 . . . . . . . . . . . . . . . . . 18 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
80 elun 3904 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥𝑦𝑥 ∈ {𝑧}))
8179, 80sylib 208 . . . . . . . . . . . . . . . . 17 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
8267, 78, 81mpjaodan 962 . . . . . . . . . . . . . . . 16 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
8382ex 397 . . . . . . . . . . . . . . 15 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8483ex 397 . . . . . . . . . . . . . 14 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8543, 84ralrimi 3106 . . . . . . . . . . . . 13 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8639, 32, 40, 85syl21anc 1475 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8738, 86jca 495 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8887ex 397 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
8988eximdv 1998 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
90 vex 3354 . . . . . . . . . . . 12 𝑓 ∈ V
91 snex 5036 . . . . . . . . . . . 12 {⟨𝑧, 𝑤⟩} ∈ V
9290, 91unex 7103 . . . . . . . . . . 11 (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
93 fneq1 6119 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
94 fveq1 6331 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
9594eleq1d 2835 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
9695imbi2d 329 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9796ralbidv 3135 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9893, 97anbi12d 608 . . . . . . . . . . 11 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
9992, 98spcev 3451 . . . . . . . . . 10 (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10099eximi 1910 . . . . . . . . 9 (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10189, 100syl6 35 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
102 ax5e 1993 . . . . . . . 8 (∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
103101, 102syl6 35 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
104103imp 393 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
105104an32s 623 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
106 fneq1 6119 . . . . . . 7 (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
107 fveq1 6331 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
108107eleq1d 2835 . . . . . . . . 9 (𝑓 = 𝑔 → ((𝑓𝑥) ∈ 𝑥 ↔ (𝑔𝑥) ∈ 𝑥))
109108imbi2d 329 . . . . . . . 8 (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
110109ralbidv 3135 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
111106, 110anbi12d 608 . . . . . 6 (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
112111cbvexvw 2126 . . . . 5 (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
113105, 112sylibr 224 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
114 simpllr 752 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧𝑦)
115 simpr 471 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
116 neq0 4077 . . . . . . . 8 𝑧 = ∅ ↔ ∃𝑤 𝑤𝑧)
117115, 116sylib 208 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤𝑧)
118 simplr 744 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119117, 118jca 495 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
120114, 119jca 495 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))))
121 eeanv 2344 . . . . . . . . 9 (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
122 simprrl 758 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
123122, 27sylib 208 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
12430a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
125 simpl 468 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ¬ 𝑧𝑦)
12633a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
127123, 124, 125, 126, 35syl121anc 1481 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
128127, 37sylibr 224 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
129 nfv 1995 . . . . . . . . . . . . . . 15 𝑥 ¬ 𝑧𝑦
130 nfv 1995 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝑧
131 nfv 1995 . . . . . . . . . . . . . . . . 17 𝑥 𝑓 Fn 𝑦
132131, 42nfan 1980 . . . . . . . . . . . . . . . 16 𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
133130, 132nfan 1980 . . . . . . . . . . . . . . 15 𝑥(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
134129, 133nfan 1980 . . . . . . . . . . . . . 14 𝑥𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
135 simpr 471 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
136 simp-4l 760 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
137135, 136jca 495 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
13850, 52syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
139137, 138syl 17 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
140 simprrr 759 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
141140adantr 466 . . . . . . . . . . . . . . . . . . . . 21 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
142141adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
143142adantr 466 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
144 simplr 744 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
145135, 143, 144, 65syl3c 66 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
146139, 145eqeltrd 2850 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
147 simplrl 754 . . . . . . . . . . . . . . . . . . . 20 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤𝑧)
148147adantr 466 . . . . . . . . . . . . . . . . . . 19 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤𝑧)
149148adantr 466 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤𝑧)
150 simpr 471 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
151150, 72syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
152 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
15430a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
15533a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
156 simp-4l 760 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧𝑦)
157122adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑓 Fn 𝑦)
158157adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑓 Fn 𝑦)
159158adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
160 fndm 6130 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 Fn 𝑦 → dom 𝑓 = 𝑦)
161159, 160syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
162156, 161neleqtrrd 2872 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
163 fsnunfv 6597 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
164154, 155, 162, 163syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
165153, 164eqtrd 2805 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
166149, 165, 1513eltr4d 2865 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
167 simplr 744 . . . . . . . . . . . . . . . . . 18 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
168167, 80sylib 208 . . . . . . . . . . . . . . . . 17 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
169146, 166, 168mpjaodan 962 . . . . . . . . . . . . . . . 16 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
170169ex 397 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
171170ex 397 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
172134, 171ralrimi 3106 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
173128, 172jca 495 . . . . . . . . . . . 12 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
174173, 99syl 17 . . . . . . . . . . 11 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
175174ex 397 . . . . . . . . . 10 𝑧𝑦 → ((𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
1761752eximdv 2000 . . . . . . . . 9 𝑧𝑦 → (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
177121, 176syl5bir 233 . . . . . . . 8 𝑧𝑦 → ((∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
178177imp 393 . . . . . . 7 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
179102exlimiv 2010 . . . . . . 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 796 . . 3 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
184183ex 397 . 2 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1854, 8, 12, 16, 26, 184findcard2s 8357 1 (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wo 826  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  Vcvv 3351  cun 3721  c0 4063  {csn 4316  cop 4322  dom cdm 5249   Fn wfn 6026  wf 6027  cfv 6031  Fincfn 8109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-om 7213  df-1o 7713  df-er 7896  df-en 8110  df-fin 8113
This theorem is referenced by:  choicefi  39910  stoweidlem31  40765  stoweidlem35  40769  stoweidlem59  40793
  Copyright terms: Public domain W3C validator