pospo

Description: Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	pospo.b	$⊢ B = {Base}_{K}$
	pospo.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pospo.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	pospo	$⊢ K \in V \to (K \in Poset \leftrightarrow (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq}))$

Proof

Step	Hyp	Ref	Expression
1		pospo.b	$⊢ B = {Base}_{K}$
2		pospo.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pospo.s	$⊢ \underset{˙}{<} = <_{K}$
4	3	pltirr	$⊢ (K \in Poset \land x \in B) \to \neg x \underset{˙}{<} x$
5	1 3	plttr	$⊢ (K \in Poset \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{<} y \land y \underset{˙}{<} z) \to x \underset{˙}{<} z)$
6	4 5	ispod	$⊢ K \in Poset \to \underset{˙}{<} Po B$
7		relres	$⊢ Rel ({I ↾}_{B})$
8	7	a1i	$⊢ K \in Poset \to Rel ({I ↾}_{B})$
9		opabresid	$⊢ {I ↾}_{B} = \{⟨x, y⟩ \| (x \in B \land y = x)\}$
10	9	eqcomi	$⊢ \{⟨x, y⟩ \| (x \in B \land y = x)\} = {I ↾}_{B}$
11	10	eleq2i	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in B \land y = x)\} \leftrightarrow ⟨x, y⟩ \in ({I ↾}_{B})$
12		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in B \land y = x)\} \leftrightarrow (x \in B \land y = x)$
13	11 12	bitr3i	$⊢ ⟨x, y⟩ \in ({I ↾}_{B}) \leftrightarrow (x \in B \land y = x)$
14	1 2	posref	$⊢ (K \in Poset \land x \in B) \to x \underset{˙}{\leq} x$
15		df-br	$⊢ x \underset{˙}{\leq} y \leftrightarrow ⟨x, y⟩ \in \underset{˙}{\leq}$
16		breq2	$⊢ y = x \to (x \underset{˙}{\leq} y \leftrightarrow x \underset{˙}{\leq} x)$
17	15 16	bitr3id	$⊢ y = x \to (⟨x, y⟩ \in \underset{˙}{\leq} \leftrightarrow x \underset{˙}{\leq} x)$
18	14 17	syl5ibrcom	$⊢ (K \in Poset \land x \in B) \to (y = x \to ⟨x, y⟩ \in \underset{˙}{\leq})$
19	18	expimpd	$⊢ K \in Poset \to ((x \in B \land y = x) \to ⟨x, y⟩ \in \underset{˙}{\leq})$
20	13 19	biimtrid	$⊢ K \in Poset \to (⟨x, y⟩ \in ({I ↾}_{B}) \to ⟨x, y⟩ \in \underset{˙}{\leq})$
21	8 20	relssdv	$⊢ K \in Poset \to {I ↾}_{B} \subseteq \underset{˙}{\leq}$
22	6 21	jca	$⊢ K \in Poset \to (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})$
23		simpl	$⊢ (K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \to K \in V$
24	1	a1i	$⊢ (K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \to B = {Base}_{K}$
25	2	a1i	$⊢ (K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \to \underset{˙}{\leq} = \leq_{K}$
26		equid	$⊢ x = x$
27		simpr	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B) \to x \in B$
28		resieq	$⊢ (x \in B \land x \in B) \to (x ({I ↾}_{B}) x \leftrightarrow x = x)$
29	27 27 28	syl2anc	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B) \to (x ({I ↾}_{B}) x \leftrightarrow x = x)$
30	26 29	mpbiri	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B) \to x ({I ↾}_{B}) x$
31		simplrr	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B) \to {I ↾}_{B} \subseteq \underset{˙}{\leq}$
32	31	ssbrd	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B) \to (x ({I ↾}_{B}) x \to x \underset{˙}{\leq} x)$
33	30 32	mpd	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B) \to x \underset{˙}{\leq} x$
34	1 2 3	pleval2i	$⊢ (x \in B \land y \in B) \to (x \underset{˙}{\leq} y \to (x \underset{˙}{<} y \lor x = y))$
35	34	3adant1	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to (x \underset{˙}{\leq} y \to (x \underset{˙}{<} y \lor x = y))$
36	1 2 3	pleval2i	$⊢ (y \in B \land x \in B) \to (y \underset{˙}{\leq} x \to (y \underset{˙}{<} x \lor y = x))$
37	36	ancoms	$⊢ (x \in B \land y \in B) \to (y \underset{˙}{\leq} x \to (y \underset{˙}{<} x \lor y = x))$
38	37	3adant1	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to (y \underset{˙}{\leq} x \to (y \underset{˙}{<} x \lor y = x))$
39		simprl	$⊢ (K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \to \underset{˙}{<} Po B$
40		po2nr	$⊢ (\underset{˙}{<} Po B \land (x \in B \land y \in B)) \to \neg (x \underset{˙}{<} y \land y \underset{˙}{<} x)$
41	40	3impb	$⊢ (\underset{˙}{<} Po B \land x \in B \land y \in B) \to \neg (x \underset{˙}{<} y \land y \underset{˙}{<} x)$
42	39 41	syl3an1	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to \neg (x \underset{˙}{<} y \land y \underset{˙}{<} x)$
43	42	pm2.21d	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to ((x \underset{˙}{<} y \land y \underset{˙}{<} x) \to x = y)$
44		simpl	$⊢ (x = y \land y \underset{˙}{<} x) \to x = y$
45	44	a1i	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to ((x = y \land y \underset{˙}{<} x) \to x = y)$
46		simpr	$⊢ (x \underset{˙}{<} y \land y = x) \to y = x$
47	46	equcomd	$⊢ (x \underset{˙}{<} y \land y = x) \to x = y$
48	47	a1i	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to ((x \underset{˙}{<} y \land y = x) \to x = y)$
49		simpl	$⊢ (x = y \land y = x) \to x = y$
50	49	a1i	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to ((x = y \land y = x) \to x = y)$
51	43 45 48 50	ccased	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to (((x \underset{˙}{<} y \lor x = y) \land (y \underset{˙}{<} x \lor y = x)) \to x = y)$
52	35 38 51	syl2and	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
53		simpr1	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to x \in B$
54		simpr2	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to y \in B$
55	53 54 34	syl2anc	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\leq} y \to (x \underset{˙}{<} y \lor x = y))$
56		simpr3	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to z \in B$
57	1 2 3	pleval2i	$⊢ (y \in B \land z \in B) \to (y \underset{˙}{\leq} z \to (y \underset{˙}{<} z \lor y = z))$
58	54 56 57	syl2anc	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to (y \underset{˙}{\leq} z \to (y \underset{˙}{<} z \lor y = z))$
59		potr	$⊢ (\underset{˙}{<} Po B \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{<} y \land y \underset{˙}{<} z) \to x \underset{˙}{<} z)$
60	39 59	sylan	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{<} y \land y \underset{˙}{<} z) \to x \underset{˙}{<} z)$
61		simpll	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to K \in V$
62	2 3	pltle	$⊢ (K \in V \land x \in B \land z \in B) \to (x \underset{˙}{<} z \to x \underset{˙}{\leq} z)$
63	61 53 56 62	syl3anc	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{<} z \to x \underset{˙}{\leq} z)$
64	60 63	syld	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{<} y \land y \underset{˙}{<} z) \to x \underset{˙}{\leq} z)$
65		breq1	$⊢ x = y \to (x \underset{˙}{<} z \leftrightarrow y \underset{˙}{<} z)$
66	65	biimpar	$⊢ (x = y \land y \underset{˙}{<} z) \to x \underset{˙}{<} z$
67	66 63	syl5	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to ((x = y \land y \underset{˙}{<} z) \to x \underset{˙}{\leq} z)$
68		breq2	$⊢ y = z \to (x \underset{˙}{<} y \leftrightarrow x \underset{˙}{<} z)$
69	68	biimpac	$⊢ (x \underset{˙}{<} y \land y = z) \to x \underset{˙}{<} z$
70	69 63	syl5	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{<} y \land y = z) \to x \underset{˙}{\leq} z)$
71	53 33	syldan	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\leq} x$
72		eqtr	$⊢ (x = y \land y = z) \to x = z$
73	72	breq2d	$⊢ (x = y \land y = z) \to (x \underset{˙}{\leq} x \leftrightarrow x \underset{˙}{\leq} z)$
74	71 73	syl5ibcom	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to ((x = y \land y = z) \to x \underset{˙}{\leq} z)$
75	64 67 70 74	ccased	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to (((x \underset{˙}{<} y \lor x = y) \land (y \underset{˙}{<} z \lor y = z)) \to x \underset{˙}{\leq} z)$
76	55 58 75	syl2and	$⊢ ((K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
77	23 24 25 33 52 76	isposd	$⊢ (K \in V \land (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})) \to K \in Poset$
78	77	ex	$⊢ K \in V \to ((\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq}) \to K \in Poset)$
79	22 78	impbid2	$⊢ K \in V \to (K \in Poset \leftrightarrow (\underset{˙}{<} Po B \land {I ↾}_{B} \subseteq \underset{˙}{\leq}))$

Metamath Proof Explorer

Theorem pospo

Proof