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 42740
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 . . . . 5 (𝜑𝐴 ∈ Fin)
2 mptfi 9118 . . . . 5 (𝐴 ∈ Fin → (𝑥𝐴𝐵) ∈ Fin)
31, 2syl 17 . . . 4 (𝜑 → (𝑥𝐴𝐵) ∈ Fin)
4 rnfi 9102 . . . 4 ((𝑥𝐴𝐵) ∈ Fin → ran (𝑥𝐴𝐵) ∈ Fin)
53, 4syl 17 . . 3 (𝜑 → ran (𝑥𝐴𝐵) ∈ Fin)
6 fnchoice 42572 . . 3 (ran (𝑥𝐴𝐵) ∈ Fin → ∃𝑔(𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)))
75, 6syl 17 . 2 (𝜑 → ∃𝑔(𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)))
8 simpl 483 . . . . 5 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → 𝜑)
9 simprl 768 . . . . 5 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → 𝑔 Fn ran (𝑥𝐴𝐵))
10 nfv 1917 . . . . . . . 8 𝑦𝜑
11 nfra1 3144 . . . . . . . 8 𝑦𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)
1210, 11nfan 1902 . . . . . . 7 𝑦(𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
13 rspa 3132 . . . . . . . . . . . 12 ((∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → (𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
1413adantll 711 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → (𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
15 vex 3436 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
16 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1716elrnmpt 5865 . . . . . . . . . . . . . . . 16 (𝑦 ∈ V → (𝑦 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑦 = 𝐵))
1815, 17ax-mp 5 . . . . . . . . . . . . . . 15 (𝑦 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑦 = 𝐵)
1918biimpi 215 . . . . . . . . . . . . . 14 (𝑦 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦 = 𝐵)
2019adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ran (𝑥𝐴𝐵)) → ∃𝑥𝐴 𝑦 = 𝐵)
21 simp3 1137 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴𝑦 = 𝐵) → 𝑦 = 𝐵)
22 choicefi.n . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵 ≠ ∅)
23223adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴𝑦 = 𝐵) → 𝐵 ≠ ∅)
2421, 23eqnetrd 3011 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑦 = 𝐵) → 𝑦 ≠ ∅)
25243exp 1118 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝐴 → (𝑦 = 𝐵𝑦 ≠ ∅)))
2625rexlimdv 3212 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑥𝐴 𝑦 = 𝐵𝑦 ≠ ∅))
2726adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ran (𝑥𝐴𝐵)) → (∃𝑥𝐴 𝑦 = 𝐵𝑦 ≠ ∅))
2820, 27mpd 15 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ≠ ∅)
2928adantlr 712 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ≠ ∅)
30 id 22 . . . . . . . . . . . 12 ((𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) → (𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))
3130imp 407 . . . . . . . . . . 11 (((𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦) ∧ 𝑦 ≠ ∅) → (𝑔𝑦) ∈ 𝑦)
3214, 29, 31syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥𝐴𝐵)) → (𝑔𝑦) ∈ 𝑦)
3332ex 413 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → (𝑦 ∈ ran (𝑥𝐴𝐵) → (𝑔𝑦) ∈ 𝑦))
3412, 33ralrimi 3141 . . . . . . . 8 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
35 rsp 3131 . . . . . . . 8 (∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦 → (𝑦 ∈ ran (𝑥𝐴𝐵) → (𝑔𝑦) ∈ 𝑦))
3634, 35syl 17 . . . . . . 7 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → (𝑦 ∈ ran (𝑥𝐴𝐵) → (𝑔𝑦) ∈ 𝑦))
3712, 36ralrimi 3141 . . . . . 6 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
3837adantrl 713 . . . . 5 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
39 vex 3436 . . . . . . . . 9 𝑔 ∈ V
4039a1i 11 . . . . . . . 8 (𝜑𝑔 ∈ V)
411mptexd 7100 . . . . . . . 8 (𝜑 → (𝑥𝐴𝐵) ∈ V)
42 coexg 7776 . . . . . . . 8 ((𝑔 ∈ V ∧ (𝑥𝐴𝐵) ∈ V) → (𝑔 ∘ (𝑥𝐴𝐵)) ∈ V)
4340, 41, 42syl2anc 584 . . . . . . 7 (𝜑 → (𝑔 ∘ (𝑥𝐴𝐵)) ∈ V)
44433ad2ant1 1132 . . . . . 6 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑔 ∘ (𝑥𝐴𝐵)) ∈ V)
45 simpr 485 . . . . . . . . 9 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → 𝑔 Fn ran (𝑥𝐴𝐵))
46 choicefi.b . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐵𝑊)
4746ralrimiva 3103 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
4816fnmpt 6573 . . . . . . . . . . 11 (∀𝑥𝐴 𝐵𝑊 → (𝑥𝐴𝐵) Fn 𝐴)
4947, 48syl 17 . . . . . . . . . 10 (𝜑 → (𝑥𝐴𝐵) Fn 𝐴)
5049adantr 481 . . . . . . . . 9 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → (𝑥𝐴𝐵) Fn 𝐴)
51 ssidd 3944 . . . . . . . . 9 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → ran (𝑥𝐴𝐵) ⊆ ran (𝑥𝐴𝐵))
52 fnco 6549 . . . . . . . . 9 ((𝑔 Fn ran (𝑥𝐴𝐵) ∧ (𝑥𝐴𝐵) Fn 𝐴 ∧ ran (𝑥𝐴𝐵) ⊆ ran (𝑥𝐴𝐵)) → (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴)
5345, 50, 51, 52syl3anc 1370 . . . . . . . 8 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵)) → (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴)
54533adant3 1131 . . . . . . 7 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴)
55 nfv 1917 . . . . . . . . 9 𝑥𝜑
56 nfcv 2907 . . . . . . . . . 10 𝑥𝑔
57 nfmpt1 5182 . . . . . . . . . . 11 𝑥(𝑥𝐴𝐵)
5857nfrn 5861 . . . . . . . . . 10 𝑥ran (𝑥𝐴𝐵)
5956, 58nffn 6532 . . . . . . . . 9 𝑥 𝑔 Fn ran (𝑥𝐴𝐵)
60 nfv 1917 . . . . . . . . . 10 𝑥(𝑔𝑦) ∈ 𝑦
6158, 60nfralw 3151 . . . . . . . . 9 𝑥𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦
6255, 59, 61nf3an 1904 . . . . . . . 8 𝑥(𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
63 funmpt 6472 . . . . . . . . . . . . . 14 Fun (𝑥𝐴𝐵)
6463a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → Fun (𝑥𝐴𝐵))
65 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝑥𝐴)
6616, 46dmmptd 6578 . . . . . . . . . . . . . . . 16 (𝜑 → dom (𝑥𝐴𝐵) = 𝐴)
6766eqcomd 2744 . . . . . . . . . . . . . . 15 (𝜑𝐴 = dom (𝑥𝐴𝐵))
6867adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 𝐴 = dom (𝑥𝐴𝐵))
6965, 68eleqtrd 2841 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥 ∈ dom (𝑥𝐴𝐵))
70 fvco 6866 . . . . . . . . . . . . 13 ((Fun (𝑥𝐴𝐵) ∧ 𝑥 ∈ dom (𝑥𝐴𝐵)) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔‘((𝑥𝐴𝐵)‘𝑥)))
7164, 69, 70syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔‘((𝑥𝐴𝐵)‘𝑥)))
7216fvmpt2 6886 . . . . . . . . . . . . . 14 ((𝑥𝐴𝐵𝑊) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7365, 46, 72syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((𝑥𝐴𝐵)‘𝑥) = 𝐵)
7473fveq2d 6778 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑔‘((𝑥𝐴𝐵)‘𝑥)) = (𝑔𝐵))
7571, 74eqtrd 2778 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔𝐵))
76753ad2antl1 1184 . . . . . . . . . 10 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) = (𝑔𝐵))
7716elrnmpt1 5867 . . . . . . . . . . . . 13 ((𝑥𝐴𝐵𝑊) → 𝐵 ∈ ran (𝑥𝐴𝐵))
7865, 46, 77syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐵 ∈ ran (𝑥𝐴𝐵))
79783ad2antl1 1184 . . . . . . . . . . 11 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → 𝐵 ∈ ran (𝑥𝐴𝐵))
80 simpl3 1192 . . . . . . . . . . 11 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦)
81 fveq2 6774 . . . . . . . . . . . . 13 (𝑦 = 𝐵 → (𝑔𝑦) = (𝑔𝐵))
82 id 22 . . . . . . . . . . . . 13 (𝑦 = 𝐵𝑦 = 𝐵)
8381, 82eleq12d 2833 . . . . . . . . . . . 12 (𝑦 = 𝐵 → ((𝑔𝑦) ∈ 𝑦 ↔ (𝑔𝐵) ∈ 𝐵))
8483rspcva 3559 . . . . . . . . . . 11 ((𝐵 ∈ ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑔𝐵) ∈ 𝐵)
8579, 80, 84syl2anc 584 . . . . . . . . . 10 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → (𝑔𝐵) ∈ 𝐵)
8676, 85eqeltrd 2839 . . . . . . . . 9 (((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) ∧ 𝑥𝐴) → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵)
8786ex 413 . . . . . . . 8 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → (𝑥𝐴 → ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
8862, 87ralrimi 3141 . . . . . . 7 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵)
8954, 88jca 512 . . . . . 6 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → ((𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
90 fneq1 6524 . . . . . . . 8 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → (𝑓 Fn 𝐴 ↔ (𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴))
91 nfcv 2907 . . . . . . . . . 10 𝑥𝑓
9256, 57nfco 5774 . . . . . . . . . 10 𝑥(𝑔 ∘ (𝑥𝐴𝐵))
9391, 92nfeq 2920 . . . . . . . . 9 𝑥 𝑓 = (𝑔 ∘ (𝑥𝐴𝐵))
94 fveq1 6773 . . . . . . . . . 10 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → (𝑓𝑥) = ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥))
9594eleq1d 2823 . . . . . . . . 9 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → ((𝑓𝑥) ∈ 𝐵 ↔ ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
9693, 95ralbid 3161 . . . . . . . 8 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵 ↔ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵))
9790, 96anbi12d 631 . . . . . . 7 (𝑓 = (𝑔 ∘ (𝑥𝐴𝐵)) → ((𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵) ↔ ((𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵)))
9897spcegv 3536 . . . . . 6 ((𝑔 ∘ (𝑥𝐴𝐵)) ∈ V → (((𝑔 ∘ (𝑥𝐴𝐵)) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝑔 ∘ (𝑥𝐴𝐵))‘𝑥) ∈ 𝐵) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)))
9944, 89, 98sylc 65 . . . . 5 ((𝜑𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑔𝑦) ∈ 𝑦) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
1008, 9, 38, 99syl3anc 1370 . . . 4 ((𝜑 ∧ (𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
101100ex 413 . . 3 (𝜑 → ((𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)))
102101exlimdv 1936 . 2 (𝜑 → (∃𝑔(𝑔 Fn ran (𝑥𝐴𝐵) ∧ ∀𝑦 ∈ ran (𝑥𝐴𝐵)(𝑦 ≠ ∅ → (𝑔𝑦) ∈ 𝑦)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)))
1037, 102mpd 15 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wex 1782  wcel 2106  wne 2943  wral 3064  wrex 3065  Vcvv 3432  wss 3887  c0 4256  cmpt 5157  dom cdm 5589  ran crn 5590  ccom 5593  Fun wfun 6427   Fn wfn 6428  cfv 6433  Fincfn 8733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-om 7713  df-1st 7831  df-2nd 7832  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-fin 8737
This theorem is referenced by:  axccdom  42762  axccd2  42769  qndenserrnbllem  43835  hoiqssbllem3  44162
  Copyright terms: Public domain W3C validator