This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acunirnmpt2f

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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
aciunf1lem.a ⊢ Ⅎ 𝑗 𝐴
acunirnmpt2f.c ⊢ Ⅎ 𝑗 𝐶
acunirnmpt2f.d ⊢ Ⅎ 𝑗 𝐷
acunirnmpt2f.2 ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵
acunirnmpt2f.3 ⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → 𝐵 = 𝐷 )
acunirnmpt2f.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion acunirnmpt2f ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 acunirnmpt.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 acunirnmpt.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
3 aciunf1lem.a ⊢ Ⅎ 𝑗 𝐴
4 acunirnmpt2f.c ⊢ Ⅎ 𝑗 𝐶
5 acunirnmpt2f.d ⊢ Ⅎ 𝑗 𝐷
6 acunirnmpt2f.2 ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵
7 acunirnmpt2f.3 ⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → 𝐵 = 𝐷 )
8 acunirnmpt2f.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
9 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
10 vex ⊢ 𝑦 ∈ V
11 eqid ⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
12 11 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 ) )
13 10 12 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
14 9 13 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
15 nfv ⊢ Ⅎ 𝑗 𝜑
16 4 nfcri ⊢ Ⅎ 𝑗 𝑥 ∈ 𝐶
17 15 16 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ 𝐶 )
18 nfcv ⊢ Ⅎ 𝑗 𝑦
19 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
20 19 nfrn ⊢ Ⅎ 𝑗 ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
21 18 20 nfel ⊢ Ⅎ 𝑗 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
22 17 21 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
23 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ 𝑦
24 22 23 nfan ⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 )
25 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 )
26 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
27 25 26 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐵 )
28 27 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑦 = 𝐵 → 𝑥 ∈ 𝐵 ) )
29 28 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑗 ∈ 𝐴 → ( 𝑦 = 𝐵 → 𝑥 ∈ 𝐵 ) ) )
30 24 29 reximdai ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
31 14 30 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
32 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 )
33 dfiun3g ⊢ ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
34 32 33 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
35 6 34 eqtrid ⊢ ( 𝜑 → 𝐶 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
36 35 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) )
37 36 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
38 eluni2 ⊢ ( 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
39 37 38 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
40 31 39 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
42 nfcv ⊢ Ⅎ 𝑘 𝐴
43 nfcv ⊢ Ⅎ 𝑘 𝐵
44 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐵
45 csbeq1a ⊢ ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑗 ⦌ 𝐵 )
46 3 42 43 44 45 cbvmptf ⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐵 )
47 mptexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑘 ∈ 𝐴 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) ∈ V )
48 46 47 eqeltrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
49 rnexg ⊢ ( ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
50 uniexg ⊢ ( ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
51 1 48 49 50 4syl ⊢ ( 𝜑 → ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
52 35 51 eqeltrd ⊢ ( 𝜑 → 𝐶 ∈ V )
53 id ⊢ ( 𝑐 = 𝐶 → 𝑐 = 𝐶 )
54 53 raleqdv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑐 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
55 53 feq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑓 : 𝑐 ⟶ 𝐴 ↔ 𝑓 : 𝐶 ⟶ 𝐴 ) )
56 53 raleqdv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ↔ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )
57 55 56 anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) ↔ ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
58 57 exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
59 54 58 imbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ∀ 𝑥 ∈ 𝑐 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) ) ↔ ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) ) )
60 5 nfcri ⊢ Ⅎ 𝑗 𝑥 ∈ 𝐷
61 vex ⊢ 𝑐 ∈ V
62 7 eleq2d ⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐷 ) )
63 3 60 61 62 ac6sf2 ⊢ ( ∀ 𝑥 ∈ 𝑐 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) )
64 59 63 vtoclg ⊢ ( 𝐶 ∈ V → ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
65 52 64 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
66 41 65 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )