Metamath Proof Explorer


Theorem acunirnmpt2

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

Ref Expression
Hypotheses acunirnmpt.0 ( 𝜑𝐴𝑉 )
acunirnmpt.1 ( ( 𝜑𝑗𝐴 ) → 𝐵 ≠ ∅ )
acunirnmpt2.2 𝐶 = ran ( 𝑗𝐴𝐵 )
acunirnmpt2.3 ( 𝑗 = ( 𝑓𝑥 ) → 𝐵 = 𝐷 )
Assertion acunirnmpt2 ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) )

Proof

Step Hyp Ref Expression
1 acunirnmpt.0 ( 𝜑𝐴𝑉 )
2 acunirnmpt.1 ( ( 𝜑𝑗𝐴 ) → 𝐵 ≠ ∅ )
3 acunirnmpt2.2 𝐶 = ran ( 𝑗𝐴𝐵 )
4 acunirnmpt2.3 ( 𝑗 = ( 𝑓𝑥 ) → 𝐵 = 𝐷 )
5 simplr ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) → 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) )
6 vex 𝑦 ∈ V
7 eqid ( 𝑗𝐴𝐵 ) = ( 𝑗𝐴𝐵 )
8 7 elrnmpt ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ↔ ∃ 𝑗𝐴 𝑦 = 𝐵 ) )
9 6 8 ax-mp ( 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ↔ ∃ 𝑗𝐴 𝑦 = 𝐵 )
10 5 9 sylib ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) → ∃ 𝑗𝐴 𝑦 = 𝐵 )
11 nfv 𝑗 ( 𝜑𝑥𝐶 )
12 nfcv 𝑗 𝑦
13 nfmpt1 𝑗 ( 𝑗𝐴𝐵 )
14 13 nfrn 𝑗 ran ( 𝑗𝐴𝐵 )
15 12 14 nfel 𝑗 𝑦 ∈ ran ( 𝑗𝐴𝐵 )
16 11 15 nfan 𝑗 ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) )
17 nfv 𝑗 𝑥𝑦
18 16 17 nfan 𝑗 ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 )
19 simpllr ( ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) ∧ 𝑗𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥𝑦 )
20 simpr ( ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) ∧ 𝑗𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
21 19 20 eleqtrd ( ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) ∧ 𝑗𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥𝐵 )
22 21 ex ( ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) ∧ 𝑗𝐴 ) → ( 𝑦 = 𝐵𝑥𝐵 ) )
23 22 ex ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) → ( 𝑗𝐴 → ( 𝑦 = 𝐵𝑥𝐵 ) ) )
24 18 23 reximdai ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) → ( ∃ 𝑗𝐴 𝑦 = 𝐵 → ∃ 𝑗𝐴 𝑥𝐵 ) )
25 10 24 mpd ( ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) ) ∧ 𝑥𝑦 ) → ∃ 𝑗𝐴 𝑥𝐵 )
26 3 eleq2i ( 𝑥𝐶𝑥 ran ( 𝑗𝐴𝐵 ) )
27 26 biimpi ( 𝑥𝐶𝑥 ran ( 𝑗𝐴𝐵 ) )
28 eluni2 ( 𝑥 ran ( 𝑗𝐴𝐵 ) ↔ ∃ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) 𝑥𝑦 )
29 27 28 sylib ( 𝑥𝐶 → ∃ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) 𝑥𝑦 )
30 29 adantl ( ( 𝜑𝑥𝐶 ) → ∃ 𝑦 ∈ ran ( 𝑗𝐴𝐵 ) 𝑥𝑦 )
31 25 30 r19.29a ( ( 𝜑𝑥𝐶 ) → ∃ 𝑗𝐴 𝑥𝐵 )
32 31 ralrimiva ( 𝜑 → ∀ 𝑥𝐶𝑗𝐴 𝑥𝐵 )
33 mptexg ( 𝐴𝑉 → ( 𝑗𝐴𝐵 ) ∈ V )
34 rnexg ( ( 𝑗𝐴𝐵 ) ∈ V → ran ( 𝑗𝐴𝐵 ) ∈ V )
35 uniexg ( ran ( 𝑗𝐴𝐵 ) ∈ V → ran ( 𝑗𝐴𝐵 ) ∈ V )
36 1 33 34 35 4syl ( 𝜑 ran ( 𝑗𝐴𝐵 ) ∈ V )
37 3 36 eqeltrid ( 𝜑𝐶 ∈ V )
38 id ( 𝑐 = 𝐶𝑐 = 𝐶 )
39 38 raleqdv ( 𝑐 = 𝐶 → ( ∀ 𝑥𝑐𝑗𝐴 𝑥𝐵 ↔ ∀ 𝑥𝐶𝑗𝐴 𝑥𝐵 ) )
40 38 feq2d ( 𝑐 = 𝐶 → ( 𝑓 : 𝑐𝐴𝑓 : 𝐶𝐴 ) )
41 38 raleqdv ( 𝑐 = 𝐶 → ( ∀ 𝑥𝑐 𝑥𝐷 ↔ ∀ 𝑥𝐶 𝑥𝐷 ) )
42 40 41 anbi12d ( 𝑐 = 𝐶 → ( ( 𝑓 : 𝑐𝐴 ∧ ∀ 𝑥𝑐 𝑥𝐷 ) ↔ ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) ) )
43 42 exbidv ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : 𝑐𝐴 ∧ ∀ 𝑥𝑐 𝑥𝐷 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) ) )
44 39 43 imbi12d ( 𝑐 = 𝐶 → ( ( ∀ 𝑥𝑐𝑗𝐴 𝑥𝐵 → ∃ 𝑓 ( 𝑓 : 𝑐𝐴 ∧ ∀ 𝑥𝑐 𝑥𝐷 ) ) ↔ ( ∀ 𝑥𝐶𝑗𝐴 𝑥𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) ) ) )
45 vex 𝑐 ∈ V
46 4 eleq2d ( 𝑗 = ( 𝑓𝑥 ) → ( 𝑥𝐵𝑥𝐷 ) )
47 45 46 ac6s ( ∀ 𝑥𝑐𝑗𝐴 𝑥𝐵 → ∃ 𝑓 ( 𝑓 : 𝑐𝐴 ∧ ∀ 𝑥𝑐 𝑥𝐷 ) )
48 44 47 vtoclg ( 𝐶 ∈ V → ( ∀ 𝑥𝐶𝑗𝐴 𝑥𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) ) )
49 37 48 syl ( 𝜑 → ( ∀ 𝑥𝐶𝑗𝐴 𝑥𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) ) )
50 32 49 mpd ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶𝐴 ∧ ∀ 𝑥𝐶 𝑥𝐷 ) )