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

Metamath Proof Explorer

Theorem ipole

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

Ref Expression
Hypotheses ipoval.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
ipole.l ⊢ ≤ = ( le ‘ 𝐼 )
Assertion ipole ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ipoval.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 ipole.l ⊢ ≤ = ( le ‘ 𝐼 )
3 preq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑥 , 𝑦 } = { 𝑋 , 𝑌 } )
4 3 sseq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( { 𝑥 , 𝑦 } ⊆ 𝐹 ↔ { 𝑋 , 𝑌 } ⊆ 𝐹 ) )
5 sseq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑌 ) )
6 4 5 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( { 𝑋 , 𝑌 } ⊆ 𝐹 ∧ 𝑋 ⊆ 𝑌 ) ) )
7 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
8 6 7 brabga ⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } 𝑌 ↔ ( { 𝑋 , 𝑌 } ⊆ 𝐹 ∧ 𝑋 ⊆ 𝑌 ) ) )
9 8 3adant1 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } 𝑌 ↔ ( { 𝑋 , 𝑌 } ⊆ 𝐹 ∧ 𝑋 ⊆ 𝑌 ) ) )
10 1 ipolerval ⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )
11 2 10 eqtr4id ⊢ ( 𝐹 ∈ 𝑉 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } )
12 11 breqd ⊢ ( 𝐹 ∈ 𝑉 → ( 𝑋 ≤ 𝑌 ↔ 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } 𝑌 ) )
13 12 3ad2ant1 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } 𝑌 ) )
14 prssi ⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → { 𝑋 , 𝑌 } ⊆ 𝐹 )
15 14 3adant1 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → { 𝑋 , 𝑌 } ⊆ 𝐹 )
16 15 biantrurd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ⊆ 𝑌 ↔ ( { 𝑋 , 𝑌 } ⊆ 𝐹 ∧ 𝑋 ⊆ 𝑌 ) ) )
17 9 13 16 3bitr4d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌 ) )