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

Metamath Proof Explorer

Theorem ipolt

Description: Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses ipolt.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
ipolt.l ⊢ < = ( lt ‘ 𝐼 )
Assertion ipolt ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ipolt.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 ipolt.l ⊢ < = ( lt ‘ 𝐼 )
3 eqid ⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
4 1 3 ipole ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ( le ‘ 𝐼 ) 𝑌 ↔ 𝑋 ⊆ 𝑌 ) )
5 4 anbi1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝑋 ( le ‘ 𝐼 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
6 1 fvexi ⊢ 𝐼 ∈ V
7 3 2 pltval ⊢ ( ( 𝐼 ∈ V ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐼 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
8 6 7 mp3an1 ⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐼 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
9 8 3adant1 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐼 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
10 df-pss ⊢ ( 𝑋 ⊊ 𝑌 ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑋 ≠ 𝑌 ) )
11 10 a1i ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ⊊ 𝑌 ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
12 5 9 11 3bitr4d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌 ) )