Theorem ipopos

Description: The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypothesis	ipopos.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
Assertion	ipopos	⊢ 𝐼 ∈ Poset

Proof

Step	Hyp	Ref	Expression
1		ipopos.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2	1	fvexi	⊢ 𝐼 ∈ V
3	2	a1i	⊢ ( 𝐹 ∈ V → 𝐼 ∈ V )
4	1	ipobas	⊢ ( 𝐹 ∈ V → 𝐹 = ( Base ‘ 𝐼 ) )
5		eqidd	⊢ ( 𝐹 ∈ V → ( le ‘ 𝐼 ) = ( le ‘ 𝐼 ) )
6		ssid	⊢ 𝑎 ⊆ 𝑎
7		eqid	⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
8	1 7	ipole	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑎 ⊆ 𝑎 ) )
9	8	3anidm23	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑎 ⊆ 𝑎 ) )
10	6 9	mpbiri	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ) → 𝑎 ( le ‘ 𝐼 ) 𝑎 )
11	1 7	ipole	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ↔ 𝑎 ⊆ 𝑏 ) )
12	1 7	ipole	⊢ ( ( 𝐹 ∈ V ∧ 𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹 ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑏 ⊆ 𝑎 ) )
13	12	3com23	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑎 ↔ 𝑏 ⊆ 𝑎 ) )
14	11 13	anbi12d	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑎 ) ↔ ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) )
15		simpl	⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) → 𝑎 ⊆ 𝑏 )
16		simpr	⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) → 𝑏 ⊆ 𝑎 )
17	15 16	eqssd	⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) → 𝑎 = 𝑏 )
18	14 17	syl6bi	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑎 ) → 𝑎 = 𝑏 ) )
19		sstr	⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑐 ) → 𝑎 ⊆ 𝑐 )
20	19	a1i	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑐 ) → 𝑎 ⊆ 𝑐 ) )
21	11	3adant3r3	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ↔ 𝑎 ⊆ 𝑏 ) )
22	1 7	ipole	⊢ ( ( 𝐹 ∈ V ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑏 ⊆ 𝑐 ) )
23	22	3adant3r1	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( 𝑏 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑏 ⊆ 𝑐 ) )
24	21 23	anbi12d	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑐 ) ↔ ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑐 ) ) )
25	1 7	ipole	⊢ ( ( 𝐹 ∈ V ∧ 𝑎 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑎 ⊆ 𝑐 ) )
26	25	3adant3r2	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( 𝑎 ( le ‘ 𝐼 ) 𝑐 ↔ 𝑎 ⊆ 𝑐 ) )
27	20 24 26	3imtr4d	⊢ ( ( 𝐹 ∈ V ∧ ( 𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹 ∧ 𝑐 ∈ 𝐹 ) ) → ( ( 𝑎 ( le ‘ 𝐼 ) 𝑏 ∧ 𝑏 ( le ‘ 𝐼 ) 𝑐 ) → 𝑎 ( le ‘ 𝐼 ) 𝑐 ) )
28	3 4 5 10 18 27	isposd	⊢ ( 𝐹 ∈ V → 𝐼 ∈ Poset )
29		fvprc	⊢ ( ¬ 𝐹 ∈ V → ( toInc ‘ 𝐹 ) = ∅ )
30	1 29	syl5eq	⊢ ( ¬ 𝐹 ∈ V → 𝐼 = ∅ )
31		0pos	⊢ ∅ ∈ Poset
32	30 31	eqeltrdi	⊢ ( ¬ 𝐹 ∈ V → 𝐼 ∈ Poset )
33	28 32	pm2.61i	⊢ 𝐼 ∈ Poset