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	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌 ) )