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 biimpi ⊢ ( 𝑦 ∈ 𝐶 → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
17 8 16 r19.29a ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ≠ ∅ )
18 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ )
19 mptexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
20 rnexg ⊢ ( ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
21 1 19 20 3syl ⊢ ( 𝜑 → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
22 3 21 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ V )
23 raleq ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑦 ∈ 𝑐 𝑦 ≠ ∅ ↔ ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ ) )
24 id ⊢ ( 𝑐 = 𝐶 → 𝑐 = 𝐶 )
25 unieq ⊢ ( 𝑐 = 𝐶 → ∪ 𝑐 = ∪ 𝐶 )
26 24 25 feq23d ⊢ ( 𝑐 = 𝐶 → ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ↔ 𝑓 : 𝐶 ⟶ ∪ 𝐶 ) )
27 raleq ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
28 26 27 anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
29 28 exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
30 23 29 imbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ∀ 𝑦 ∈ 𝑐 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) ) )
31 vex ⊢ 𝑐 ∈ V
32 31 ac5b ⊢ ( ∀ 𝑦 ∈ 𝑐 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ ∪ 𝑐 ∧ ∀ 𝑦 ∈ 𝑐 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
33 30 32 vtoclg ⊢ ( 𝐶 ∈ V → ( ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
34 22 33 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ) )
35 18 34 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) )
36 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
37 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 )
38 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
39 37 38 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 )
40 39 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑦 = 𝐵 → ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
41 40 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
42 36 41 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 )
43 42 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
44 43 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 → ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )
45 44 anim2d ⊢ ( 𝜑 → ( ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) ) )
46 45 eximdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑓 ‘ 𝑦 ) ∈ 𝑦 ) → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) ) )
47 35 46 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ ∪ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ 𝐵 ) )