Metamath Proof Explorer

Theorem csbxp

Description: Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbxp ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
2 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
3 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
4 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
5 sbcg ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ) )
6 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) )
7 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
8 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
9 7 8 anbi12i ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
10 6 9 bitri ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
11 10 a1i ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
12 5 11 anbi12d ⊢ ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
13 sbcex ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ V )
14 13 con3i ⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
15 14 intnand ⊢ ( ¬ 𝐴 ∈ V → ¬ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
16 noel ⊢ ¬ 𝑦 ∈ ∅
17 16 a1i ⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ∅ )
18 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ∅ )
19 17 18 neleqtrrd ⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
20 19 intnand ⊢ ( ¬ 𝐴 ∈ V → ¬ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
21 20 intnand ⊢ ( ¬ 𝐴 ∈ V → ¬ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
22 15 21 2falsed ⊢ ( ¬ 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
23 12 22 pm2.61i ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
24 4 23 bitri ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
25 24 exbii ⊢ ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
26 3 25 bitri ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
27 26 exbii ⊢ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
28 2 27 bitri ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
29 28 abbii ⊢ { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) }
30 1 29 eqtri ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) }
31 df-xp ⊢ ( 𝐵 × 𝐶 ) = { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) }
32 df-opab ⊢ { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
33 31 32 eqtri ⊢ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
34 33 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
35 df-xp ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) }
36 df-opab ⊢ { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) }
37 35 36 eqtri ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) }
38 30 34 37 3eqtr4i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )