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

Metamath Proof Explorer

Theorem cdleme31so

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 25-Feb-2013)

Ref Expression
Hypotheses cdleme31so.o ⊢ 𝑂 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
cdleme31so.c ⊢ 𝐶 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
Assertion cdleme31so ( 𝑋 ∈ 𝐵 → ⦋ 𝑋 / 𝑥 ⦌ 𝑂 = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme31so.o ⊢ 𝑂 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
2 cdleme31so.c ⊢ 𝐶 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
3 nfcvd ⊢ ( 𝑋 ∈ 𝐵 → Ⅎ 𝑥 ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
4 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ 𝑊 ) = ( 𝑋 ∧ 𝑊 ) )
5 4 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) )
6 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ↔ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
8 7 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) )
9 4 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) )
10 9 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ↔ 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
11 8 10 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ↔ ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
12 11 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ↔ ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
13 12 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
14 3 13 csbiegf ⊢ ( 𝑋 ∈ 𝐵 → ⦋ 𝑋 / 𝑥 ⦌ ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
15 1 csbeq2i ⊢ ⦋ 𝑋 / 𝑥 ⦌ 𝑂 = ⦋ 𝑋 / 𝑥 ⦌ ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
16 14 15 2 3eqtr4g ⊢ ( 𝑋 ∈ 𝐵 → ⦋ 𝑋 / 𝑥 ⦌ 𝑂 = 𝐶 )