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	⊢ ( 𝑋 ∈ 𝐵 → ⦋ 𝑋 / 𝑥 ⦌ 𝑂 = 𝐶 )