Metamath Proof Explorer

Theorem acunirnmpt

Description: Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019)

Ref Expression
Hypotheses acunirnmpt.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
acunirnmpt.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
acunirnmpt.2 ⊢ 𝐶 = ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
Assertion acunirnmpt ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 acunirnmpt.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 acunirnmpt.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
3 acunirnmpt.2 ⊢ 𝐶 = ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
4 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
5 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝜑 )
6 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑗 ∈ 𝐴 )
7 5 6 2 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝐵 ≠ ∅ )
8 4 7 eqnetrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 ≠ ∅ )
9 3 eleq2i ⊢ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
10 vex ⊢ 𝑦 ∈ V
11 eqid ⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
12 11 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 ) )
13 10 12 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
14 9 13 bitri ⊢ ( 𝑦 ∈ 𝐶 ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
15 14 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
16 8 15 r19.29a ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ≠ ∅ )
17 16 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ )
18 mptexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
19 rnexg ⊢ ( ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
20 1 18 19 3syl ⊢ ( 𝜑 → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
21 3 20 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ V )
22 raleq ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑦 ∈ 𝑐 𝑦 ≠ ∅ ↔ ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ ) )
23 id ⊢ ( 𝑐 = 𝐶 → 𝑐 = 𝐶 )
24 unieq ⊢ ( 𝑐 = 𝐶 → ∪ 𝑐 = ∪ 𝐶 )
25 23 24 feq23d ⊢ ( 𝑐 = 𝐶 → ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ↔ 𝑓 : 𝐶 ⟶ ∪ 𝐶 ) )
26 raleq ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
27 25 26 anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
28 27 exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
29 22 28 imbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ∀ 𝑦 ∈ 𝑐 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ) )
30 vex ⊢ 𝑐 ∈ V
31 30 ac5b ⊢ ( ∀ 𝑦 ∈ 𝑐 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
32 29 31 vtoclg ⊢ ( 𝐶 ∈ V → ( ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
33 21 32 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
34 17 33 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
35 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
36 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
37 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
38 36 37 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 )
39 38 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑦 = 𝐵 → ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
40 39 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
41 35 40 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 )
42 41 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
43 42 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
44 43 anim2d ⊢ ( 𝜑 → ( ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) ) )
45 44 eximdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) ) )
46 34 45 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )