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

Metamath Proof Explorer

Theorem csbnestgfw

Description: Nest the composition of two substitutions. Version of csbnestgf with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 23-Nov-2005) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Assertion csbnestgfw ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2 df-csb ⊢ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 }
3 2 eqabri ⊢ ( 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 )
4 3 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 )
5 nfcr ⊢ ( Ⅎ 𝑥 𝐶 → Ⅎ 𝑥 𝑧 ∈ 𝐶 )
6 5 alimi ⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝐶 → ∀ 𝑦 Ⅎ 𝑥 𝑧 ∈ 𝐶 )
7 sbcnestgfw ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝑧 ∈ 𝐶 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ) )
8 6 7 sylan2 ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ) )
9 4 8 bitrid ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ) )
10 9 abbidv ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 } = { 𝑧 ∣ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 } )
11 1 10 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 } = { 𝑧 ∣ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 } )
12 df-csb ⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 }
13 df-csb ⊢ ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 }
14 11 12 13 3eqtr4g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ 𝐶 )