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

Metamath Proof Explorer

Theorem cdleme31fv

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

Ref Expression
Hypotheses cdleme31.o ⊢ 𝑂 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
cdleme31.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
cdleme31.c ⊢ 𝐶 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
Assertion cdleme31fv ( 𝑋 ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cdleme31.o ⊢ 𝑂 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
2 cdleme31.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
3 cdleme31.c ⊢ 𝐶 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
4 riotaex ⊢ ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) ∈ V
5 3 4 eqeltri ⊢ 𝐶 ∈ V
6 ifexg ⊢ ( ( 𝐶 ∈ V ∧ 𝑋 ∈ 𝐵 ) → if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) ∈ V )
7 5 6 mpan ⊢ ( 𝑋 ∈ 𝐵 → if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) ∈ V )
8 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑊 ↔ 𝑋 ≤ 𝑊 ) )
9 8 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ≤ 𝑊 ↔ ¬ 𝑋 ≤ 𝑊 ) )
10 9 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) )
11 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ 𝑊 ) = ( 𝑋 ∧ 𝑊 ) )
12 11 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) )
13 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
14 12 13 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ↔ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
15 14 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) ↔ ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) )
16 11 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) )
17 16 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ↔ 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
18 15 17 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ↔ ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
19 18 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ↔ ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
20 19 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) ) )
21 20 1 3 3eqtr4g ⊢ ( 𝑥 = 𝑋 → 𝑂 = 𝐶 )
22 10 21 13 ifbieq12d ⊢ ( 𝑥 = 𝑋 → if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) = if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) )
23 22 2 fvmptg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) ∈ V ) → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) )
24 7 23 mpdan ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) )