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 ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )