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

Theorem choicefi 45205
Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
choicefi.a (𝜑𝐴 ∈ Fin)
choicefi.b ((𝜑𝑥𝐴) → 𝐵𝑊)
choicefi.n ((𝜑𝑥𝐴) → 𝐵 ≠ ∅)
Assertion
Ref Expression
choicefi (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
Distinct variable groups:   𝐴,𝑓,𝑥   𝐵,𝑓   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑥)   𝑊(𝑥,𝑓)

Proof of Theorem choicefi
Dummy variables 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 choicefi.a . . 3 (𝜑𝐴 ∈ Fin)
2 mptfi 9391 . . 3 (𝐴 ∈ Fin → (𝑥𝐴𝐵) ∈ Fin)
3 rnfi 9380 . . 3 ((𝑥𝐴𝐵) ∈ Fin → ran (𝑥𝐴𝐵) ∈ Fin)
4 fnchoice 45034 . . 3 (ran (𝑥𝐴𝐵) ∈ Fin → ∃𝑔(𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)))
51, 2, 3, 44syl 19 . 2 (𝜑 → ∃𝑔(𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)))
6 simpl 482 . . . . 5 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → 𝜑)
7 simprl 771 . . . . 5 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → 𝑔 Fn ran (𝑥𝐴𝐵))
8 nfv 1914 . . . . . . . 8 𝑦𝜑
9 nfra1 3284 . . . . . . . 8 𝑦𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)
108, 9nfan 1899 . . . . . . 7 𝑦(𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
11 rspa 3248 . . . . . . . . . . . 12 ((∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → (𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
1211adantll 714 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → (𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
13 vex 3484 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
14 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1514elrnmpt 5969 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (𝑦 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑦 = 𝐵))
1613, 15ax-mp 5 . . . . . . . . . . . . . . 15 (𝑦 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑦 = 𝐵)
1716biimpi 216 . . . . . . . . . . . . . 14 (𝑦 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦 = 𝐵)
1817adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ran (𝑥𝐴𝐵)) → ∃𝑥𝐴 𝑦 = 𝐵)
19 simp3 1139 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴𝑦 = 𝐵) → 𝑦 = 𝐵)
20 choicefi.n . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 ≠ ∅)
21203adant3 1133 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴𝑦 = 𝐵) → 𝐵 ≠ ∅)
2219, 21eqnetrd 3008 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑦 = 𝐵) → 𝑦 ≠ ∅)
23223exp 1120 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → (𝑦 = 𝐵𝑦 ≠ ∅)))
2423rexlimdv 3153 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑥𝐴 𝑦 = 𝐵𝑦 ≠ ∅))
2524adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ran (𝑥𝐴𝐵)) → (∃𝑥𝐴 𝑦 = 𝐵𝑦 ≠ ∅))
2618, 25mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ≠ ∅)
2726adantlr 715 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ≠ ∅)
28 id 22 . . . . . . . . . . . 12 ((𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) → (𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
2928imp 406 . . . . . . . . . . 11 (((𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ 𝑦 ≠ ∅) → (𝑔𝑦) ∈ 𝑦)
3012, 27, 29syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → (𝑔𝑦) ∈ 𝑦)
3130ex 412 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → (𝑦 ∈ ran (𝑥𝐴𝐵) → (𝑔𝑦) ∈ 𝑦))
3210, 31ralrimi 3257 . . . . . . . 8 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
33 rsp 3247 . . . . . . . 8 (∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦 → (𝑦 ∈ ran (𝑥𝐴𝐵) → (𝑔𝑦) ∈ 𝑦))
3432, 33syl 17 . . . . . . 7 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → (𝑦 ∈ ran (𝑥𝐴𝐵) → (𝑔𝑦) ∈ 𝑦))
3510, 34ralrimi 3257 . . . . . 6 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
3635adantrl 716 . . . . 5 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
37 vex 3484 . . . . . . . . 9 𝑔 ∈ V
3837a1i 11 . . . . . . . 8 (𝜑𝑔 ∈ V)
391mptexd 7244 . . . . . . . 8 (𝜑 → (𝑥𝐴𝐵) ∈ V)
40 coexg 7951 . . . . . . . 8 ((𝑔 ∈ V ∧ (𝑥𝐴𝐵) ∈ V) → (𝑔 ∘ (𝑥𝐴𝐵)) ∈ V)
4138, 39, 40syl2anc 584 . . . . . . 7 (𝜑 → (𝑔 ∘ (𝑥𝐴𝐵)) ∈ V)
42413ad2ant1 1134 . . . . . 6 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑔 ∘ (𝑥𝐴𝐵)) ∈ V)
43 simpr 484 . . . . . . . . 9 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → 𝑔 Fn ran (𝑥𝐴𝐵))
44 choicefi.b . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐵𝑊)
4544ralrimiva 3146 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
4614fnmpt 6708 . . . . . . . . . . 11 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
4745, 46syl 17 . . . . . . . . . 10 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
4847adantr 480 . . . . . . . . 9 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → (𝑥𝐴𝐵) Fn 𝐴)
49 ssidd 4007 . . . . . . . . 9 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → ran (𝑥𝐴𝐵) ⊆ ran (𝑥𝐴𝐵))
50 fnco 6686 . . . . . . . . 9 ((𝑔 Fn ran (𝑥𝐴𝐵) ∧ (𝑥𝐴𝐵) Fn 𝐴 ∧ ran (𝑥𝐴𝐵) ⊆ ran (𝑥𝐴𝐵)) → (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴)
5143, 48, 49, 50syl3anc 1373 . . . . . . . 8 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴)
52513adant3 1133 . . . . . . 7 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴)
53 nfv 1914 . . . . . . . . 9 𝑥𝜑
54 nfcv 2905 . . . . . . . . . 10 𝑥𝑔
55 nfmpt1 5250 . . . . . . . . . . 11 𝑥(𝑥𝐴𝐵)
5655nfrn 5963 . . . . . . . . . 10 𝑥ran (𝑥𝐴𝐵)
5754, 56nffn 6667 . . . . . . . . 9 𝑥 𝑔 Fn ran (𝑥𝐴𝐵)
58 nfv 1914 . . . . . . . . . 10 𝑥(𝑔𝑦) ∈ 𝑦
5956, 58nfralw 3311 . . . . . . . . 9 𝑥𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦
6053, 57, 59nf3an 1901 . . . . . . . 8 𝑥(𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
61 funmpt 6604 . . . . . . . . . . . . . 14 Fun (𝑥𝐴𝐵)
6261a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun (𝑥𝐴𝐵))
63 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑥𝐴)
6414, 44dmmptd 6713 . . . . . . . . . . . . . . . 16 (𝜑 → dom (𝑥𝐴𝐵) = 𝐴)
6564eqcomd 2743 . . . . . . . . . . . . . . 15 (𝜑𝐴 = dom (𝑥𝐴𝐵))
6665adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = dom (𝑥𝐴𝐵))
6763, 66eleqtrd 2843 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥 ∈ dom (𝑥𝐴𝐵))
68 fvco 7007 . . . . . . . . . . . . 13 ((Fun (𝑥𝐴𝐵) ∧ 𝑥 ∈ dom (𝑥𝐴𝐵)) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔‘((𝑥𝐴𝐵)‘𝑥)))
6962, 67, 68syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔‘((𝑥𝐴𝐵)‘𝑥)))
7014fvmpt2 7027 . . . . . . . . . . . . . 14 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7163, 44, 70syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7271fveq2d 6910 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑔‘((𝑥𝐴𝐵)‘𝑥)) = (𝑔𝐵))
7369, 72eqtrd 2777 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔𝐵))
74733ad2antl1 1186 . . . . . . . . . 10 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔𝐵))
7514elrnmpt1 5971 . . . . . . . . . . . . 13 ((𝑥𝐴𝐵𝑊) → 𝐵 ∈ ran (𝑥𝐴𝐵))
7663, 44, 75syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐵 ∈ ran (𝑥𝐴𝐵))
77763ad2antl1 1186 . . . . . . . . . . 11 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → 𝐵 ∈ ran (𝑥𝐴𝐵))
78 simpl3 1194 . . . . . . . . . . 11 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
79 fveq2 6906 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑔𝑦) = (𝑔𝐵))
80 id 22 . . . . . . . . . . . . 13 (𝑦 = 𝐵𝑦 = 𝐵)
8179, 80eleq12d 2835 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ((𝑔𝑦) ∈ 𝑦 ↔ (𝑔𝐵) ∈ 𝐵))
8281rspcva 3620 . . . . . . . . . . 11 ((𝐵 ∈ ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑔𝐵) ∈ 𝐵)
8377, 78, 82syl2anc 584 . . . . . . . . . 10 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → (𝑔𝐵) ∈ 𝐵)
8474, 83eqeltrd 2841 . . . . . . . . 9 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵)
8584ex 412 . . . . . . . 8 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑥𝐴 → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
8660, 85ralrimi 3257 . . . . . . 7 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵)
8752, 86jca 511 . . . . . 6 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → ((𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
88 fneq1 6659 . . . . . . . 8 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → (𝑓 Fn 𝐴 ↔ (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴))
89 nfcv 2905 . . . . . . . . . 10 𝑥𝑓
9054, 55nfco 5876 . . . . . . . . . 10 𝑥(𝑔 ∘ (𝑥𝐴𝐵))
9189, 90nfeq 2919 . . . . . . . . 9 𝑥 𝑓 = (𝑔 ∘ (𝑥𝐴𝐵))
92 fveq1 6905 . . . . . . . . . 10 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → (𝑓𝑥) = ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥))
9392eleq1d 2826 . . . . . . . . 9 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → ((𝑓𝑥) ∈ 𝐵 ↔ ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
9491, 93ralbid 3273 . . . . . . . 8 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 ↔ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
9588, 94anbi12d 632 . . . . . . 7 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → ((𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) ↔ ((𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵)))
9695spcegv 3597 . . . . . 6 ((𝑔 ∘ (𝑥𝐴𝐵)) ∈ V → (((𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)))
9742, 87, 96sylc 65 . . . . 5 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
986, 7, 36, 97syl3anc 1373 . . . 4 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
9998ex 412 . . 3 (𝜑 → ((𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)))
10099exlimdv 1933 . 2 (𝜑 → (∃𝑔(𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)))
1015, 100mpd 15 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  wss 3951  c0 4333  cmpt 5225  dom cdm 5685  ran crn 5686  ccom 5689  Fun wfun 6555   Fn wfn 6556  cfv 6561  Fincfn 8985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1st 8014  df-2nd 8015  df-1o 8506  df-en 8986  df-dom 8987  df-fin 8989
This theorem is referenced by:  axccdom  45227  axccd2  45235  qndenserrnbllem  46309  hoiqssbllem3  46639
  Copyright terms: Public domain W3C validator