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

Metamath Proof Explorer

Theorem fmpox

Description: Functionality, domain and codomain of a class given by the maps-to notation, where B ( x ) is not constant but depends on x . (Contributed by NM, 29-Dec-2014)

Ref Expression
Hypothesis fmpox.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion fmpox ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 )

Proof

Step Hyp Ref Expression
1 fmpox.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 vex ⊢ 𝑧 ∈ V
3 vex ⊢ 𝑤 ∈ V
4 2 3 op1std ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 1st ‘ 𝑣 ) = 𝑧 )
5 4 csbeq1d ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 )
6 2 3 op2ndd ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 2nd ‘ 𝑣 ) = 𝑤 )
7 6 csbeq1d ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
8 7 csbeq2dv ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ 𝑧 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
9 5 8 eqtrd ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
10 9 eleq1d ⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
11 10 raliunxp ⊢ ( ∀ 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
12 nfv ⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 )
13 nfv ⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 )
14 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
15 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
16 15 nfcri ⊢ Ⅎ 𝑥 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵
17 14 16 nfan ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
18 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
19 18 nfeq2 ⊢ Ⅎ 𝑥 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
20 17 19 nfan ⊢ Ⅎ 𝑥 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
21 nfv ⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
22 nfcv ⊢ Ⅎ 𝑦 𝑧
23 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝐶
24 22 23 nfcsbw ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
25 24 nfeq2 ⊢ Ⅎ 𝑦 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
26 21 25 nfan ⊢ Ⅎ 𝑦 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
27 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
28 27 adantr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
29 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
30 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
31 30 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
32 29 31 sylan9bbr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
33 28 32 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
34 csbeq1a ⊢ ( 𝑦 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
35 csbeq1a ⊢ ( 𝑥 = 𝑧 → ⦋ 𝑤 / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
36 34 35 sylan9eqr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
37 36 eqeq2d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 = 𝐶 ↔ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) )
38 33 37 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) ) )
39 12 13 20 26 38 cbvoprab12 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) } = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) }
40 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) }
41 df-mpo ⊢ ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) }
42 39 40 41 3eqtr4i ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
43 9 mpomptx ⊢ ( 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
44 42 1 43 3eqtr4i ⊢ 𝐹 = ( 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 )
45 44 fmpt ⊢ ( ∀ 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 )
46 11 45 bitr3i ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 )
47 nfv ⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷
48 18 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷
49 15 48 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷
50 nfv ⊢ Ⅎ 𝑤 𝐶 ∈ 𝐷
51 23 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷
52 34 eleq1d ⊢ ( 𝑦 = 𝑤 → ( 𝐶 ∈ 𝐷 ↔ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
53 50 51 52 cbvralw ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ 𝐵 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
54 35 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
55 30 54 raleqbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
56 53 55 bitrid ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
57 47 49 56 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
58 nfcv ⊢ Ⅎ 𝑧 ( { 𝑥 } × 𝐵 )
59 nfcv ⊢ Ⅎ 𝑥 { 𝑧 }
60 59 15 nfxp ⊢ Ⅎ 𝑥 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
61 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
62 61 30 xpeq12d ⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } × 𝐵 ) = ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
63 58 60 62 cbviun ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
64 63 feq2i ⊢ ( 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 )
65 46 57 64 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 )