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 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.
StepHypRef Expression
1 fneq2 6563 . . . 4 (𝑤 = ∅ → (𝑓 Fn 𝑤𝑓 Fn ∅))
2 raleq 3305 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
31, 2anbi12d 631 . . 3 (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
43exbidv 1923 . 2 (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
5 fneq2 6563 . . . 4 (𝑤 = 𝑦 → (𝑓 Fn 𝑤𝑓 Fn 𝑦))
6 raleq 3305 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
75, 6anbi12d 631 . . 3 (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
87exbidv 1923 . 2 (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
9 fneq2 6563 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤𝑓 Fn (𝑦 ∪ {𝑧})))
10 raleq 3305 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119, 10anbi12d 631 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1211exbidv 1923 . 2 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
13 fneq2 6563 . . . 4 (𝑤 = 𝐴 → (𝑓 Fn 𝑤𝑓 Fn 𝐴))
14 raleq 3305 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
1513, 14anbi12d 631 . . 3 (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1615exbidv 1923 . 2 (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
17 0ex 5245 . . . 4 ∅ ∈ V
18 fneq1 6562 . . . 4 (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19 eqid 2736 . . . . 5 ∅ = ∅
20 fn0 6601 . . . . 5 (∅ Fn ∅ ↔ ∅ = ∅)
2119, 20mpbir 230 . . . 4 ∅ Fn ∅
2217, 18, 21ceqsexv2d 3489 . . 3 𝑓 𝑓 Fn ∅
23 ral0 4454 . . 3 𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
2422, 23exan 1864 . 2 𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
25 dffn2 6639 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2625biimpi 215 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2726ad2antrl 725 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28 vex 3444 . . . . . . . . . . . . . . 15 𝑧 ∈ V
2928a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30 simpllr 773 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ¬ 𝑧𝑦)
31 vex 3444 . . . . . . . . . . . . . . 15 𝑤 ∈ V
3231a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33 fsnunf 7096 . . . . . . . . . . . . . 14 ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3427, 29, 30, 32, 33syl121anc 1374 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35 dffn2 6639 . . . . . . . . . . . . 13 ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3634, 35sylibr 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 𝑥𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
4139, 40nfan 1901 . . . . . . . . . . . . . 14 𝑥((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
42 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
43 simpllr 773 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧𝑦)
4443adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧𝑦)
4544adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
4642, 45jca 512 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
47 nelne2 3039 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑥𝑧)
4847necomd 2996 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑥)
4946, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑧𝑥)
50 fvunsn 7090 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
5149, 50syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
52 simpllr 773 . . . . . . . . . . . . . . . . . . . 20 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
5352adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
54 simplr 766 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
55 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56 fveq2 6811 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑥 → (𝑓𝑢) = (𝑓𝑥))
5756eleq1d 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑢))
58 eleq2w 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑥) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
5957, 58bitrd 278 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6055, 59imbi12d 344 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6160cbvralvw 3221 . . . . . . . . . . . . . . . . . . . 20 (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
6260rspcv 3565 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6361, 62syl5bir 242 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 → (∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6442, 53, 54, 63syl3c 66 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
6551, 64eqeltrd 2837 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66 simp-4l 780 . . . . . . . . . . . . . . . . . . 19 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
6766adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69 simplr 766 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70 elsni 4587 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71703ad2ant2 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72 simp1 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
7371, 72eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74 simp3 1137 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
7573, 74pm2.21ddne 3026 . . . . . . . . . . . . . . . . . 18 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
7667, 68, 69, 75syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77 simplr 766 . . . . . . . . . . . . . . . . . 18 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78 elun 4093 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥𝑦𝑥 ∈ {𝑧}))
7977, 78sylib 217 . . . . . . . . . . . . . . . . 17 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
8065, 76, 79mpjaodan 956 . . . . . . . . . . . . . . . 16 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
8180ex 413 . . . . . . . . . . . . . . 15 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8281ex 413 . . . . . . . . . . . . . 14 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8341, 82ralrimi 3236 . . . . . . . . . . . . 13 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8437, 30, 38, 83syl21anc 835 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8536, 84jca 512 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8685ex 413 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
8786eximdv 1919 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88 vex 3444 . . . . . . . . . . . 12 𝑓 ∈ V
89 snex 5368 . . . . . . . . . . . 12 {⟨𝑧, 𝑤⟩} ∈ V
9088, 89unex 7637 . . . . . . . . . . 11 (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91 fneq1 6562 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92 fveq1 6810 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
9392eleq1d 2821 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
9493imbi2d 340 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9594ralbidv 3170 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9691, 95anbi12d 631 . . . . . . . . . . 11 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
9790, 96spcev 3553 . . . . . . . . . 10 (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
9897eximi 1836 . . . . . . . . 9 (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
9987, 98syl6 35 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
100 ax5e 1914 . . . . . . . 8 (∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10199, 100syl6 35 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
102101imp 407 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
103102an32s 649 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
104 fneq1 6562 . . . . . . 7 (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105 fveq1 6810 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
106105eleq1d 2821 . . . . . . . . 9 (𝑓 = 𝑔 → ((𝑓𝑥) ∈ 𝑥 ↔ (𝑔𝑥) ∈ 𝑥))
107106imbi2d 340 . . . . . . . 8 (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
108107ralbidv 3170 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
109104, 108anbi12d 631 . . . . . 6 (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
110109cbvexvw 2039 . . . . 5 (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
111103, 110sylibr 233 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
112 simpllr 773 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧𝑦)
113 simpr 485 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114 neq0 4289 . . . . . . . 8 𝑧 = ∅ ↔ ∃𝑤 𝑤𝑧)
115113, 114sylib 217 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤𝑧)
116 simplr 766 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
117115, 116jca 512 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
118112, 117jca 512 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))))
119 exdistrv 1958 . . . . . . . . 9 (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
120 simprrl 778 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121120, 25sylib 217 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
12228a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
123 simpl 483 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ¬ 𝑧𝑦)
12431a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
125121, 122, 123, 124, 33syl121anc 1374 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126125, 35sylibr 233 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127 nfv 1916 . . . . . . . . . . . . . . 15 𝑥 ¬ 𝑧𝑦
128 nfv 1916 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝑧
129 nfv 1916 . . . . . . . . . . . . . . . . 17 𝑥 𝑓 Fn 𝑦
130129, 40nfan 1901 . . . . . . . . . . . . . . . 16 𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
131128, 130nfan 1901 . . . . . . . . . . . . . . 15 𝑥(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
132127, 131nfan 1901 . . . . . . . . . . . . . 14 𝑥𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
133 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
134 simp-4l 780 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
135133, 134jca 512 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
13648, 50syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
137135, 136syl 17 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
138 simprrr 779 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
139138ad5ant12 753 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
140 simplr 766 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
141133, 139, 140, 63syl3c 66 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
142137, 141eqeltrd 2837 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143 simplrl 774 . . . . . . . . . . . . . . . . . . . 20 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤𝑧)
144143adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤𝑧)
145144adantr 481 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤𝑧)
146 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
147146, 70syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
148 fveq2 6811 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
15028a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
15131a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
152 simp-4l 780 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧𝑦)
153120ad5ant12 753 . . . . . . . . . . . . . . . . . . . . . 22 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154153fndmd 6576 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155152, 154neleqtrrd 2859 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156 fsnunfv 7098 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157150, 151, 155, 156syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158149, 157eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159145, 158, 1473eltr4d 2852 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160 simplr 766 . . . . . . . . . . . . . . . . . 18 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161160, 78sylib 217 . . . . . . . . . . . . . . . . 17 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
162142, 159, 161mpjaodan 956 . . . . . . . . . . . . . . . 16 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163162ex 413 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164163ex 413 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165132, 164ralrimi 3236 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
166126, 165jca 512 . . . . . . . . . . . 12 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
167166, 97syl 17 . . . . . . . . . . 11 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
168167ex 413 . . . . . . . . . 10 𝑧𝑦 → ((𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
1691682eximdv 1921 . . . . . . . . 9 𝑧𝑦 → (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
170119, 169syl5bir 242 . . . . . . . 8 𝑧𝑦 → ((∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
171170imp 407 . . . . . . 7 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
172100exlimiv 1932 . . . . . . 7 (∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
173171, 172syl 17 . . . . . 6 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
174173, 110sylibr 233 . . . . 5 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
175118, 174syl 17 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
176111, 175pm2.61dan 810 . . 3 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
177176ex 413 . 2 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1784, 8, 12, 16, 24, 177findcard2s 9008 1 (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator