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 ( ( 𝑃𝑄 ∧ ¬ 𝑋 𝑊 ) , 𝐶 , 𝑋 ) )