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