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