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 41163
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 6438 . . . 4 (𝑤 = ∅ → (𝑓 Fn 𝑤𝑓 Fn ∅))
2 raleq 3403 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
31, 2anbi12d 630 . . 3 (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
43exbidv 1913 . 2 (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
5 fneq2 6438 . . . 4 (𝑤 = 𝑦 → (𝑓 Fn 𝑤𝑓 Fn 𝑦))
6 raleq 3403 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
75, 6anbi12d 630 . . 3 (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
87exbidv 1913 . 2 (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
9 fneq2 6438 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤𝑓 Fn (𝑦 ∪ {𝑧})))
10 raleq 3403 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119, 10anbi12d 630 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1211exbidv 1913 . 2 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
13 fneq2 6438 . . . 4 (𝑤 = 𝐴 → (𝑓 Fn 𝑤𝑓 Fn 𝐴))
14 raleq 3403 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
1513, 14anbi12d 630 . . 3 (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1615exbidv 1913 . 2 (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
17 0ex 5202 . . . 4 ∅ ∈ V
18 fneq1 6437 . . . 4 (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19 eqid 2818 . . . . 5 ∅ = ∅
20 fn0 6472 . . . . 5 (∅ Fn ∅ ↔ ∅ = ∅)
2119, 20mpbir 232 . . . 4 ∅ Fn ∅
2217, 18, 21ceqsexv2d 3540 . . 3 𝑓 𝑓 Fn ∅
23 ral0 4452 . . 3 𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
2422, 23exan 1853 . 2 𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
25 dffn2 6509 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2625biimpi 217 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2726ad2antrl 724 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28 vex 3495 . . . . . . . . . . . . . . 15 𝑧 ∈ V
2928a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30 simpllr 772 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ¬ 𝑧𝑦)
31 vex 3495 . . . . . . . . . . . . . . 15 𝑤 ∈ V
3231a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33 fsnunf 6939 . . . . . . . . . . . . . 14 ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3427, 29, 30, 32, 33syl121anc 1367 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35 dffn2 6509 . . . . . . . . . . . . 13 ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3634, 35sylibr 235 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37 simplr 765 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38 simprr 769 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
39 nfv 1906 . . . . . . . . . . . . . . 15 𝑥(𝑧 = ∅ ∧ ¬ 𝑧𝑦)
40 nfra1 3216 . . . . . . . . . . . . . . 15 𝑥𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
4139, 40nfan 1891 . . . . . . . . . . . . . 14 𝑥((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
42 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
43 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧𝑦)
4443adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧𝑦)
4544adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
4642, 45jca 512 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
47 nelne2 3112 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑥𝑧)
4847necomd 3068 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑥)
4946, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑧𝑥)
50 fvunsn 6933 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
5149, 50syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
52 simpllr 772 . . . . . . . . . . . . . . . . . . . 20 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
5352adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
54 simplr 765 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
55 neeq1 3075 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑥 → (𝑓𝑢) = (𝑓𝑥))
5756eleq1d 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑢))
58 eleq2w 2893 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑥) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
5957, 58bitrd 280 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6055, 59imbi12d 346 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6160cbvralvw 3447 . . . . . . . . . . . . . . . . . . . 20 (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
6260rspcv 3615 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6361, 62syl5bir 244 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 → (∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6442, 53, 54, 63syl3c 66 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
6551, 64eqeltrd 2910 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66 simp-4l 779 . . . . . . . . . . . . . . . . . . 19 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
6766adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69 simplr 765 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70 elsni 4574 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71703ad2ant2 1126 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72 simp1 1128 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
7371, 72eqtrd 2853 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74 simp3 1130 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
7573, 74pm2.21ddne 3098 . . . . . . . . . . . . . . . . . 18 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
7667, 68, 69, 75syl3anc 1363 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77 simplr 765 . . . . . . . . . . . . . . . . . 18 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78 elun 4122 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥𝑦𝑥 ∈ {𝑧}))
7977, 78sylib 219 . . . . . . . . . . . . . . . . 17 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
8065, 76, 79mpjaodan 952 . . . . . . . . . . . . . . . 16 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
8180ex 413 . . . . . . . . . . . . . . 15 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8281ex 413 . . . . . . . . . . . . . 14 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8341, 82ralrimi 3213 . . . . . . . . . . . . 13 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8437, 30, 38, 83syl21anc 833 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8536, 84jca 512 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8685ex 413 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
8786eximdv 1909 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88 vex 3495 . . . . . . . . . . . 12 𝑓 ∈ V
89 snex 5322 . . . . . . . . . . . 12 {⟨𝑧, 𝑤⟩} ∈ V
9088, 89unex 7458 . . . . . . . . . . 11 (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91 fneq1 6437 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92 fveq1 6662 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
9392eleq1d 2894 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
9493imbi2d 342 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9594ralbidv 3194 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9691, 95anbi12d 630 . . . . . . . . . . 11 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
9790, 96spcev 3604 . . . . . . . . . 10 (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
9897eximi 1826 . . . . . . . . 9 (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
9987, 98syl6 35 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
100 ax5e 1904 . . . . . . . 8 (∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10199, 100syl6 35 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
102101imp 407 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
103102an32s 648 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
104 fneq1 6437 . . . . . . 7 (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105 fveq1 6662 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
106105eleq1d 2894 . . . . . . . . 9 (𝑓 = 𝑔 → ((𝑓𝑥) ∈ 𝑥 ↔ (𝑔𝑥) ∈ 𝑥))
107106imbi2d 342 . . . . . . . 8 (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
108107ralbidv 3194 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
109104, 108anbi12d 630 . . . . . 6 (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
110109cbvexvw 2035 . . . . 5 (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
111103, 110sylibr 235 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
112 simpllr 772 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧𝑦)
113 simpr 485 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114 neq0 4306 . . . . . . . 8 𝑧 = ∅ ↔ ∃𝑤 𝑤𝑧)
115113, 114sylib 219 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤𝑧)
116 simplr 765 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
117115, 116jca 512 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
118112, 117jca 512 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))))
119 exdistrv 1947 . . . . . . . . 9 (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
120 simprrl 777 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121120, 25sylib 219 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
12228a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
123 simpl 483 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ¬ 𝑧𝑦)
12431a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
125121, 122, 123, 124, 33syl121anc 1367 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126125, 35sylibr 235 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127 nfv 1906 . . . . . . . . . . . . . . 15 𝑥 ¬ 𝑧𝑦
128 nfv 1906 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝑧
129 nfv 1906 . . . . . . . . . . . . . . . . 17 𝑥 𝑓 Fn 𝑦
130129, 40nfan 1891 . . . . . . . . . . . . . . . 16 𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
131128, 130nfan 1891 . . . . . . . . . . . . . . 15 𝑥(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
132127, 131nfan 1891 . . . . . . . . . . . . . 14 𝑥𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
133 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
134 simp-4l 779 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
135133, 134jca 512 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
13648, 50syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
137135, 136syl 17 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
138 simprrr 778 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
139138ad5ant12 752 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
140 simplr 765 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
141133, 139, 140, 63syl3c 66 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
142137, 141eqeltrd 2910 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143 simplrl 773 . . . . . . . . . . . . . . . . . . . 20 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤𝑧)
144143adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤𝑧)
145144adantr 481 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤𝑧)
146 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
147146, 70syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
148 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
15028a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
15131a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
152 simp-4l 779 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧𝑦)
153120ad5ant12 752 . . . . . . . . . . . . . . . . . . . . . 22 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154153fndmd 6449 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155152, 154neleqtrrd 2932 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156 fsnunfv 6941 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157150, 151, 155, 156syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158149, 157eqtrd 2853 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159145, 158, 1473eltr4d 2925 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160 simplr 765 . . . . . . . . . . . . . . . . . 18 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161160, 78sylib 219 . . . . . . . . . . . . . . . . 17 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
162142, 159, 161mpjaodan 952 . . . . . . . . . . . . . . . 16 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163162ex 413 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164163ex 413 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165132, 164ralrimi 3213 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
166126, 165jca 512 . . . . . . . . . . . 12 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
167166, 97syl 17 . . . . . . . . . . 11 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
168167ex 413 . . . . . . . . . 10 𝑧𝑦 → ((𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
1691682eximdv 1911 . . . . . . . . 9 𝑧𝑦 → (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
170119, 169syl5bir 244 . . . . . . . 8 𝑧𝑦 → ((∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
171170imp 407 . . . . . . 7 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
172100exlimiv 1922 . . . . . . 7 (∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
173171, 172syl 17 . . . . . 6 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
174173, 110sylibr 235 . . . . 5 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
175118, 174syl 17 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
176111, 175pm2.61dan 809 . . 3 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
177176ex 413 . 2 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1784, 8, 12, 16, 24, 177findcard2s 8747 1 (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wne 3013  wral 3135  Vcvv 3492  cun 3931  c0 4288  {csn 4557  cop 4563  dom cdm 5548   Fn wfn 6343  wf 6344  cfv 6348  Fincfn 8497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7570  df-1o 8091  df-er 8278  df-en 8498  df-fin 8501
This theorem is referenced by:  choicefi  41339  stoweidlem31  42193  stoweidlem35  42197  stoweidlem59  42221
  Copyright terms: Public domain W3C validator