Theorem ipolerval

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

	Ref	Expression
Hypothesis	ipoval.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
Assertion	ipolerval	⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	prss	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐹 )
5	4	biranri	⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) )
6	5	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) }
7		df-xp	⊢ ( 𝐹 × 𝐹 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) }
8	6 7	sseqtrri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ ( 𝐹 × 𝐹 )
9		sqxpexg	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 × 𝐹 ) ∈ V )
10		ssexg	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ ( 𝐹 × 𝐹 ) ∧ ( 𝐹 × 𝐹 ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V )
11	8 9 10	sylancr	⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V )
12		ipostr	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) Struct ⟨ 1 , ; 1 1 ⟩
13		pleid	⊢ le = Slot ( le ‘ ndx )
14		snsspr1	⊢ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ } ⊆ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ }
15		ssun2	⊢ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
16	14 15	sstri	⊢ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
17	12 13 16	strfv	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
18	11 17	syl	⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
19		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
20	1 19	ipoval	⊢ ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
21	20	fveq2d	⊢ ( 𝐹 ∈ 𝑉 → ( le ‘ 𝐼 ) = ( le ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
22	18 21	eqtr4d	⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )