Theorem cdleme31sn1c

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

	Ref	Expression
Hypotheses	cdleme31sn1c.g	⊢ 𝐺 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐸 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdleme31sn1c.i	⊢ 𝐼 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) )
	cdleme31sn1c.n	⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
	cdleme31sn1c.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐸 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdleme31sn1c.c	⊢ 𝐶 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝑌 ) )
Assertion	cdleme31sn1c	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		cdleme31sn1c.g	⊢ 𝐺 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐸 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
2		cdleme31sn1c.i	⊢ 𝐼 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) )
3		cdleme31sn1c.n	⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
4		cdleme31sn1c.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐸 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) )
5		cdleme31sn1c.c	⊢ 𝐶 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝑌 ) )
6		eqid	⊢ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) )
7	2 3 6	cdleme31sn1	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
8	1 4	cdleme31se	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐺 = 𝑌 )
9	8	adantr	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝐺 = 𝑌 )
10	9	eqeq2d	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ↔ 𝑦 = 𝑌 ) )
11	10	imbi2d	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ↔ ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝑌 ) ) )
12	11	ralbidv	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ↔ ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝑌 ) ) )
13	12	riotabidv	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝑌 ) ) )
14	13 5	eqtr4di	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) = 𝐶 )
15	7 14	eqtrd	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )