Theorem ipoval

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

	Ref	Expression
Hypotheses	ipoval.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
	ipoval.l	⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
Assertion	ipoval	⊢ ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipoval.l	⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
3		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
4		vex	⊢ 𝑓 ∈ V
5	4 4	xpex	⊢ ( 𝑓 × 𝑓 ) ∈ V
6		simpl	⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) → { 𝑥 , 𝑦 } ⊆ 𝑓 )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	prss	⊢ ( ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑓 )
10	6 9	sylibr	⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) )
11	10	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) }
12		df-xp	⊢ ( 𝑓 × 𝑓 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) }
13	11 12	sseqtrri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ ( 𝑓 × 𝑓 )
14	5 13	ssexi	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V
15	14	a1i	⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V )
16		sseq2	⊢ ( 𝑓 = 𝐹 → ( { 𝑥 , 𝑦 } ⊆ 𝑓 ↔ { 𝑥 , 𝑦 } ⊆ 𝐹 ) )
17	16	anbi1d	⊢ ( 𝑓 = 𝐹 → ( ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) ) )
18	17	opabbidv	⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } )
19	18 2	eqtr4di	⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } = ≤ )
20		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → 𝑓 = 𝐹 )
21	20	opeq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ )
22		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → 𝑜 = ≤ )
23	22	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ( ordTop ‘ 𝑜 ) = ( ordTop ‘ ≤ ) )
24	23	opeq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ )
25	21 24	preq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } )
26	22	opeq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( le ‘ ndx ) , 𝑜 ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
27		id	⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
28		rabeq	⊢ ( 𝑓 = 𝐹 → { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } = { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } )
29	28	unieqd	⊢ ( 𝑓 = 𝐹 → ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } = ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } )
30	27 29	mpteq12dv	⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) = ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) )
31	30	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) = ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) )
32	31	opeq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ = ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ )
33	26 32	preq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } = { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
34	25 33	uneq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
35	15 19 34	csbied2	⊢ ( 𝑓 = 𝐹 → ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
36		df-ipo	⊢ toInc = ( 𝑓 ∈ V ↦ ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
37		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∈ V
38		prex	⊢ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ∈ V
39	37 38	unex	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ∈ V
40	35 36 39	fvmpt	⊢ ( 𝐹 ∈ V → ( toInc ‘ 𝐹 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
41	1 40	syl5eq	⊢ ( 𝐹 ∈ V → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
42	3 41	syl	⊢ ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )