Metamath Proof Explorer

Theorem mpoeq123

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013) (Revised by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion mpoeq123 ( ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑥 𝐴 = 𝐷
2 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 )
3 1 2 nfan ⊢ Ⅎ 𝑥 ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) )
4 nfv ⊢ Ⅎ 𝑦 𝐴 = 𝐷
5 nfcv ⊢ Ⅎ 𝑦 𝐴
6 nfv ⊢ Ⅎ 𝑦 𝐵 = 𝐸
7 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹
8 6 7 nfan ⊢ Ⅎ 𝑦 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 )
9 5 8 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 )
10 4 9 nfan ⊢ Ⅎ 𝑦 ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) )
11 nfv ⊢ Ⅎ 𝑧 ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) )
12 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) ) )
13 rsp ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 → ( 𝑦 ∈ 𝐵 → 𝐶 = 𝐹 ) )
14 eqeq2 ⊢ ( 𝐶 = 𝐹 → ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐹 ) )
15 13 14 syl6 ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 → ( 𝑦 ∈ 𝐵 → ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐹 ) ) )
16 15 pm5.32d ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐹 ) ) )
17 eleq2 ⊢ ( 𝐵 = 𝐸 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐸 ) )
18 17 anbi1d ⊢ ( 𝐵 = 𝐸 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐹 ) ↔ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) )
19 16 18 sylan9bbr ⊢ ( ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) )
20 12 19 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) ) )
21 20 pm5.32d ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) ) )
22 eleq2 ⊢ ( 𝐴 = 𝐷 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐷 ) )
23 22 anbi1d ⊢ ( 𝐴 = 𝐷 → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) ) )
24 21 23 sylan9bbr ⊢ ( ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) ) )
25 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 = 𝐶 ) ) )
26 anass ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝑦 ∈ 𝐸 ∧ 𝑧 = 𝐹 ) ) )
27 24 25 26 3bitr4g ⊢ ( ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) ) )
28 3 10 11 27 oprabbid ⊢ ( ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) } )
29 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
30 df-mpo ⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 = 𝐹 ) }
31 28 29 30 3eqtr4g ⊢ ( ( 𝐴 = 𝐷 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 = 𝐸 ∧ ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐹 ) ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ 𝐸 ↦ 𝐹 ) )