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 44456
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 6641 . . . 4 (𝑤 = ∅ → (𝑓 Fn 𝑤𝑓 Fn ∅))
2 raleq 3312 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
31, 2anbi12d 630 . . 3 (𝑤 = ∅ → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
43exbidv 1916 . 2 (𝑤 = ∅ → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
5 fneq2 6641 . . . 4 (𝑤 = 𝑦 → (𝑓 Fn 𝑤𝑓 Fn 𝑦))
6 raleq 3312 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
75, 6anbi12d 630 . . 3 (𝑤 = 𝑦 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
87exbidv 1916 . 2 (𝑤 = 𝑦 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
9 fneq2 6641 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑓 Fn 𝑤𝑓 Fn (𝑦 ∪ {𝑧})))
10 raleq 3312 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
119, 10anbi12d 630 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1211exbidv 1916 . 2 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
13 fneq2 6641 . . . 4 (𝑤 = 𝐴 → (𝑓 Fn 𝑤𝑓 Fn 𝐴))
14 raleq 3312 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
1513, 14anbi12d 630 . . 3 (𝑤 = 𝐴 → ((𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1615exbidv 1916 . 2 (𝑤 = 𝐴 → (∃𝑓(𝑓 Fn 𝑤 ∧ ∀𝑥𝑤 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
17 0ex 5302 . . . 4 ∅ ∈ V
18 fneq1 6640 . . . 4 (𝑓 = ∅ → (𝑓 Fn ∅ ↔ ∅ Fn ∅))
19 eqid 2725 . . . . 5 ∅ = ∅
20 fn0 6681 . . . . 5 (∅ Fn ∅ ↔ ∅ = ∅)
2119, 20mpbir 230 . . . 4 ∅ Fn ∅
2217, 18, 21ceqsexv2d 3518 . . 3 𝑓 𝑓 Fn ∅
23 ral0 4508 . . 3 𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
2422, 23exan 1857 . 2 𝑓(𝑓 Fn ∅ ∧ ∀𝑥 ∈ ∅ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
25 dffn2 6719 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2625biimpi 215 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑦𝑓:𝑦⟶V)
2726ad2antrl 726 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑓:𝑦⟶V)
28 vex 3467 . . . . . . . . . . . . . . 15 𝑧 ∈ V
2928a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 ∈ V)
30 simpllr 774 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ¬ 𝑧𝑦)
31 vex 3467 . . . . . . . . . . . . . . 15 𝑤 ∈ V
3231a1i 11 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑤 ∈ V)
33 fsnunf 7190 . . . . . . . . . . . . . 14 ((𝑓:𝑦⟶V ∧ (𝑧 ∈ V ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ V) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3427, 29, 30, 32, 33syl121anc 1372 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
35 dffn2 6719 . . . . . . . . . . . . 13 ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
3634, 35sylibr 233 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
37 simplr 767 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → 𝑧 = ∅)
38 simprr 771 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
39 nfv 1909 . . . . . . . . . . . . . . 15 𝑥(𝑧 = ∅ ∧ ¬ 𝑧𝑦)
40 nfra1 3272 . . . . . . . . . . . . . . 15 𝑥𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)
4139, 40nfan 1894 . . . . . . . . . . . . . 14 𝑥((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
42 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
43 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → ¬ 𝑧𝑦)
4443adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ¬ 𝑧𝑦)
4544adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
4642, 45jca 510 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
47 nelne2 3030 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑥𝑧)
4847necomd 2986 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑥)
4946, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑧𝑥)
50 fvunsn 7184 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
5149, 50syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
52 simpllr 774 . . . . . . . . . . . . . . . . . . . 20 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
5352adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
54 simplr 767 . . . . . . . . . . . . . . . . . . 19 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
55 neeq1 2993 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → (𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅))
56 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑥 → (𝑓𝑢) = (𝑓𝑥))
5756eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑢))
58 eleq2w 2809 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑥 → ((𝑓𝑥) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
5957, 58bitrd 278 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑥 → ((𝑓𝑢) ∈ 𝑢 ↔ (𝑓𝑥) ∈ 𝑥))
6055, 59imbi12d 343 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑥 → ((𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6160cbvralvw 3225 . . . . . . . . . . . . . . . . . . . 20 (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) ↔ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
6260rspcv 3597 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑦 → (∀𝑢𝑦 (𝑢 ≠ ∅ → (𝑓𝑢) ∈ 𝑢) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6361, 62biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 → (∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) → (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
6442, 53, 54, 63syl3c 66 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
6551, 64eqeltrd 2825 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
66 simp-4l 781 . . . . . . . . . . . . . . . . . . 19 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
6766adantr 479 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 = ∅)
68 simpr 483 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
69 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ≠ ∅)
70 elsni 4641 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
71703ad2ant2 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = 𝑧)
72 simp1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑧 = ∅)
7371, 72eqtrd 2765 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 = ∅)
74 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅)
7573, 74pm2.21ddne 3016 . . . . . . . . . . . . . . . . . 18 ((𝑧 = ∅ ∧ 𝑥 ∈ {𝑧} ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
7667, 68, 69, 75syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
77 simplr 767 . . . . . . . . . . . . . . . . . 18 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
78 elun 4141 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑥𝑦𝑥 ∈ {𝑧}))
7977, 78sylib 217 . . . . . . . . . . . . . . . . 17 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
8065, 76, 79mpjaodan 956 . . . . . . . . . . . . . . . 16 (((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
8180ex 411 . . . . . . . . . . . . . . 15 ((((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8281ex 411 . . . . . . . . . . . . . 14 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8341, 82ralrimi 3245 . . . . . . . . . . . . 13 (((𝑧 = ∅ ∧ ¬ 𝑧𝑦) ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8437, 30, 38, 83syl21anc 836 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
8536, 84jca 510 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
8685ex 411 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → ((𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
8786eximdv 1912 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
88 vex 3467 . . . . . . . . . . . 12 𝑓 ∈ V
89 snex 5427 . . . . . . . . . . . 12 {⟨𝑧, 𝑤⟩} ∈ V
9088, 89unex 7746 . . . . . . . . . . 11 (𝑓 ∪ {⟨𝑧, 𝑤⟩}) ∈ V
91 fneq1 6640 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔 Fn (𝑦 ∪ {𝑧}) ↔ (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧})))
92 fveq1 6891 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥))
9392eleq1d 2810 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔𝑥) ∈ 𝑥 ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
9493imbi2d 339 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9594ralbidv 3168 . . . . . . . . . . . 12 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
9691, 95anbi12d 630 . . . . . . . . . . 11 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑤⟩}) → ((𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ↔ ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))))
9790, 96spcev 3585 . . . . . . . . . 10 (((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
9897eximi 1829 . . . . . . . . 9 (∃𝑓((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
9987, 98syl6 35 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
100 ax5e 1907 . . . . . . . 8 (∃𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
10199, 100syl6 35 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
102101imp 405 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑧 = ∅) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
103102an32s 650 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
104 fneq1 6640 . . . . . . 7 (𝑓 = 𝑔 → (𝑓 Fn (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (𝑦 ∪ {𝑧})))
105 fveq1 6891 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
106105eleq1d 2810 . . . . . . . . 9 (𝑓 = 𝑔 → ((𝑓𝑥) ∈ 𝑥 ↔ (𝑔𝑥) ∈ 𝑥))
107106imbi2d 339 . . . . . . . 8 (𝑓 = 𝑔 → ((𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
108107ralbidv 3168 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥) ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
109104, 108anbi12d 630 . . . . . 6 (𝑓 = 𝑔 → ((𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ (𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
110109cbvexvw 2032 . . . . 5 (∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) ↔ ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
111103, 110sylibr 233 . . . 4 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ 𝑧 = ∅) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
112 simpllr 774 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧𝑦)
113 simpr 483 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ¬ 𝑧 = ∅)
114 neq0 4341 . . . . . . . 8 𝑧 = ∅ ↔ ∃𝑤 𝑤𝑧)
115113, 114sylib 217 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑤 𝑤𝑧)
116 simplr 767 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
117115, 116jca 510 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
118112, 117jca 510 . . . . 5 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ∧ ¬ 𝑧 = ∅) → (¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))))
119 exdistrv 1951 . . . . . . . . 9 (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) ↔ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
120 simprrl 779 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓 Fn 𝑦)
121120, 25sylib 217 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑓:𝑦⟶V)
12228a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑧 ∈ V)
123 simpl 481 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ¬ 𝑧𝑦)
12431a1i 11 . . . . . . . . . . . . . . 15 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → 𝑤 ∈ V)
125121, 122, 123, 124, 33syl121anc 1372 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}):(𝑦 ∪ {𝑧})⟶V)
126125, 35sylibr 233 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}))
127 nfv 1909 . . . . . . . . . . . . . . 15 𝑥 ¬ 𝑧𝑦
128 nfv 1909 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝑧
129 nfv 1909 . . . . . . . . . . . . . . . . 17 𝑥 𝑓 Fn 𝑦
130129, 40nfan 1894 . . . . . . . . . . . . . . . 16 𝑥(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
131128, 130nfan 1894 . . . . . . . . . . . . . . 15 𝑥(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
132127, 131nfan 1894 . . . . . . . . . . . . . 14 𝑥𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
133 simpr 483 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥𝑦)
134 simp-4l 781 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ¬ 𝑧𝑦)
135133, 134jca 510 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑥𝑦 ∧ ¬ 𝑧𝑦))
13648, 50syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ¬ 𝑧𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
137135, 136syl 17 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = (𝑓𝑥))
138 simprrr 780 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
139138ad5ant12 754 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))
140 simplr 767 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → 𝑥 ≠ ∅)
141133, 139, 140, 63syl3c 66 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → (𝑓𝑥) ∈ 𝑥)
142137, 141eqeltrd 2825 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥𝑦) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
143 simplrl 775 . . . . . . . . . . . . . . . . . . . 20 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → 𝑤𝑧)
144143adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑤𝑧)
145144adantr 479 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤𝑧)
146 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 ∈ {𝑧})
147146, 70syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑥 = 𝑧)
148 fveq2 6892 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧))
15028a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑧 ∈ V)
15131a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑤 ∈ V)
152 simp-4l 781 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧𝑦)
153120ad5ant12 754 . . . . . . . . . . . . . . . . . . . . . 22 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → 𝑓 Fn 𝑦)
154153fndmd 6654 . . . . . . . . . . . . . . . . . . . . 21 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → dom 𝑓 = 𝑦)
155152, 154neleqtrrd 2848 . . . . . . . . . . . . . . . . . . . 20 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ¬ 𝑧 ∈ dom 𝑓)
156 fsnunfv 7192 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
157150, 151, 155, 156syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑧) = 𝑤)
158149, 157eqtrd 2765 . . . . . . . . . . . . . . . . . 18 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) = 𝑤)
159145, 158, 1473eltr4d 2840 . . . . . . . . . . . . . . . . 17 (((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) ∧ 𝑥 ∈ {𝑧}) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
160 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧}))
161160, 78sylib 217 . . . . . . . . . . . . . . . . 17 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → (𝑥𝑦𝑥 ∈ {𝑧}))
162142, 159, 161mpjaodan 956 . . . . . . . . . . . . . . . 16 ((((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑥 ≠ ∅) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)
163162ex 411 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) ∧ 𝑥 ∈ (𝑦 ∪ {𝑧})) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
164163ex 411 . . . . . . . . . . . . . 14 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → (𝑥 ∈ (𝑦 ∪ {𝑧}) → (𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
165132, 164ralrimi 3245 . . . . . . . . . . . . 13 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥))
166126, 165jca 510 . . . . . . . . . . . 12 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ((𝑓 ∪ {⟨𝑧, 𝑤⟩}) Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → ((𝑓 ∪ {⟨𝑧, 𝑤⟩})‘𝑥) ∈ 𝑥)))
167166, 97syl 17 . . . . . . . . . . 11 ((¬ 𝑧𝑦 ∧ (𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
168167ex 411 . . . . . . . . . 10 𝑧𝑦 → ((𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
1691682eximdv 1914 . . . . . . . . 9 𝑧𝑦 → (∃𝑤𝑓(𝑤𝑧 ∧ (𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
170119, 169biimtrrid 242 . . . . . . . 8 𝑧𝑦 → ((∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))))
171170imp 405 . . . . . . 7 ((¬ 𝑧𝑦 ∧ (∃𝑤 𝑤𝑧 ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))) → ∃𝑤𝑓𝑔(𝑔 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
172100exlimiv 1925 . . . . . . 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 811 . . 3 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ ∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
177176ex 411 . 2 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∃𝑓(𝑓 Fn 𝑦 ∧ ∀𝑥𝑦 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)) → ∃𝑓(𝑓 Fn (𝑦 ∪ {𝑧}) ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})(𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥))))
1784, 8, 12, 16, 24, 177findcard2s 9188 1 (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑓𝑥) ∈ 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2930  wral 3051  Vcvv 3463  cun 3937  c0 4318  {csn 4624  cop 4630  dom cdm 5672   Fn wfn 6538  wf 6539  cfv 6543  Fincfn 8962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5294  ax-nul 5301  ax-pr 5423  ax-un 7738
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5144  df-opab 5206  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7869  df-en 8963  df-fin 8966
This theorem is referenced by:  choicefi  44637  stoweidlem31  45482  stoweidlem35  45486  stoweidlem59  45510
  Copyright terms: Public domain W3C validator