Metamath Proof Explorer

Theorem dibelval3

Description: Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014)

Ref Expression
Hypotheses dibval3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dibval3.l ⊢ ≤ = ( le ‘ 𝐾 )
dibval3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dibval3.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dibval3.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dibval3.o ⊢ 0 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dibval3.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion dibelval3 ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑋 ) ↔ ∃ 𝑓 ∈ 𝑇 ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dibval3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dibval3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dibval3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dibval3.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 dibval3.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 dibval3.o ⊢ 0 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7 dibval3.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
9 1 2 3 4 6 8 7 dibval2 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { 0 } ) )
10 9 eleq2d ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑋 ) ↔ 𝑌 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { 0 } ) ) )
11 1 2 3 4 5 8 diaelval ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ↔ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) )
12 11 anbi1d ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) ) )
13 an13 ⊢ ( ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) ↔ ( 𝑠 ∈ { 0 } ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ) )
14 velsn ⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
15 14 anbi1i ⊢ ( ( 𝑠 ∈ { 0 } ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ) ↔ ( 𝑠 = 0 ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ) )
16 13 15 bitri ⊢ ( ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) ↔ ( 𝑠 = 0 ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ) )
17 16 exbii ⊢ ( ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) ↔ ∃ 𝑠 ( 𝑠 = 0 ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ) )
18 4 fvexi ⊢ 𝑇 ∈ V
19 18 mptex ⊢ ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ∈ V
20 6 19 eqeltri ⊢ 0 ∈ V
21 opeq2 ⊢ ( 𝑠 = 0 → ⟨ 𝑓 , 𝑠 ⟩ = ⟨ 𝑓 , 0 ⟩ )
22 21 eqeq2d ⊢ ( 𝑠 = 0 → ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ↔ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) )
23 22 anbi2d ⊢ ( 𝑠 = 0 → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) ) )
24 20 23 ceqsexv ⊢ ( ∃ 𝑠 ( 𝑠 = 0 ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) )
25 17 24 bitri ⊢ ( ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) )
26 anass ⊢ ( ( ( 𝑓 ∈ 𝑇 ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ↔ ( 𝑓 ∈ 𝑇 ∧ ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) )
27 an32 ⊢ ( ( ( 𝑓 ∈ 𝑇 ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) )
28 26 27 bitr3i ⊢ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ∧ 𝑌 = ⟨ 𝑓 , 0 ⟩ ) )
29 12 25 28 3bitr4g ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) ↔ ( 𝑓 ∈ 𝑇 ∧ ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) ) )
30 29 exbidv ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ∃ 𝑓 ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) ↔ ∃ 𝑓 ( 𝑓 ∈ 𝑇 ∧ ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) ) )
31 elxp ⊢ ( 𝑌 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { 0 } ) ↔ ∃ 𝑓 ∃ 𝑠 ( 𝑌 = ⟨ 𝑓 , 𝑠 ⟩ ∧ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∧ 𝑠 ∈ { 0 } ) ) )
32 df-rex ⊢ ( ∃ 𝑓 ∈ 𝑇 ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ↔ ∃ 𝑓 ( 𝑓 ∈ 𝑇 ∧ ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) )
33 30 31 32 3bitr4g ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { 0 } ) ↔ ∃ 𝑓 ∈ 𝑇 ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) )
34 10 33 bitrd ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑋 ) ↔ ∃ 𝑓 ∈ 𝑇 ( 𝑌 = ⟨ 𝑓 , 0 ⟩ ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) )