opsrtoslem2

	Ref	Expression
Hypotheses	opsrso.o	$⊢ O = (I ordPwSer R) (T)$
	opsrso.i	$⊢ φ \to I \in V$
	opsrso.r	$⊢ φ \to R \in Toset$
	opsrso.t	$⊢ φ \to T \subseteq I \times I$
	opsrso.w	$⊢ φ \to T We I$
	opsrtoslem.s	$⊢ S = I mPwSer R$
	opsrtoslem.b	$⊢ B = {Base}_{S}$
	opsrtoslem.q	$⊢ \underset{˙}{<} = <_{R}$
	opsrtoslem.c	$⊢ C = T <_{bag} I$
	opsrtoslem.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	opsrtoslem.ps	$⊢ ψ \leftrightarrow \exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w)))$
	opsrtoslem.l	$⊢ \underset{˙}{\leq} = \leq_{O}$
Assertion	opsrtoslem2	$⊢ φ \to O \in Toset$

Proof

Step	Hyp	Ref	Expression
1		opsrso.o	$⊢ O = (I ordPwSer R) (T)$
2		opsrso.i	$⊢ φ \to I \in V$
3		opsrso.r	$⊢ φ \to R \in Toset$
4		opsrso.t	$⊢ φ \to T \subseteq I \times I$
5		opsrso.w	$⊢ φ \to T We I$
6		opsrtoslem.s	$⊢ S = I mPwSer R$
7		opsrtoslem.b	$⊢ B = {Base}_{S}$
8		opsrtoslem.q	$⊢ \underset{˙}{<} = <_{R}$
9		opsrtoslem.c	$⊢ C = T <_{bag} I$
10		opsrtoslem.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
11		opsrtoslem.ps	$⊢ ψ \leftrightarrow \exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w)))$
12		opsrtoslem.l	$⊢ \underset{˙}{\leq} = \leq_{O}$
13		ovex	$⊢ {ℕ_{0}}^{I} \in V$
14	10 13	rabex2	$⊢ D \in V$
15	2 2	xpexd	$⊢ φ \to I \times I \in V$
16	15 4	ssexd	$⊢ φ \to T \in V$
17	9 10 2 16 5	ltbwe	$⊢ φ \to C We D$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19		eqid	$⊢ \leq_{R} = \leq_{R}$
20	18 19 8	tosso	$⊢ R \in Toset \to (R \in Toset \leftrightarrow (\underset{˙}{<} Or {Base}_{R} \land {I ↾}_{{Base}_{R}} \subseteq \leq_{R}))$
21	20	ibi	$⊢ R \in Toset \to (\underset{˙}{<} Or {Base}_{R} \land {I ↾}_{{Base}_{R}} \subseteq \leq_{R})$
22	3 21	syl	$⊢ φ \to (\underset{˙}{<} Or {Base}_{R} \land {I ↾}_{{Base}_{R}} \subseteq \leq_{R})$
23	22	simpld	$⊢ φ \to \underset{˙}{<} Or {Base}_{R}$
24	11	opabbii	$⊢ \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| \exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w)))\}$
25	24	wemapso	$⊢ (D \in V \land C We D \land \underset{˙}{<} Or {Base}_{R}) \to \{⟨x, y⟩ \| ψ\} Or ({Base}_{R}^{D})$
26	14 17 23 25	mp3an2i	$⊢ φ \to \{⟨x, y⟩ \| ψ\} Or ({Base}_{R}^{D})$
27	6 18 10 7 2	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
28		soeq2	$⊢ B = {Base}_{R}^{D} \to (\{⟨x, y⟩ \| ψ\} Or B \leftrightarrow \{⟨x, y⟩ \| ψ\} Or ({Base}_{R}^{D}))$
29	27 28	syl	$⊢ φ \to (\{⟨x, y⟩ \| ψ\} Or B \leftrightarrow \{⟨x, y⟩ \| ψ\} Or ({Base}_{R}^{D}))$
30	26 29	mpbird	$⊢ φ \to \{⟨x, y⟩ \| ψ\} Or B$
31		soinxp	$⊢ \{⟨x, y⟩ \| ψ\} Or B \leftrightarrow (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) Or B$
32	30 31	sylib	$⊢ φ \to (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) Or B$
33	1	fvexi	$⊢ O \in V$
34		eqid	$⊢ <_{O} = <_{O}$
35	12 34	pltfval	$⊢ O \in V \to <_{O} = \underset{˙}{\leq} ∖ I$
36	33 35	ax-mp	$⊢ <_{O} = \underset{˙}{\leq} ∖ I$
37		difundir	$⊢ ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})) ∖ I = ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I) \cup (({I ↾}_{B}) ∖ I)$
38		resss	$⊢ {I ↾}_{B} \subseteq I$
39		ssdif0	$⊢ {I ↾}_{B} \subseteq I \leftrightarrow ({I ↾}_{B}) ∖ I = \emptyset$
40	38 39	mpbi	$⊢ ({I ↾}_{B}) ∖ I = \emptyset$
41	40	uneq2i	$⊢ ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I) \cup (({I ↾}_{B}) ∖ I) = ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I) \cup \emptyset$
42		un0	$⊢ ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I) \cup \emptyset = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I$
43	37 41 42	3eqtri	$⊢ ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})) ∖ I = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I$
44	1 2 3 4 5 6 7 8 9 10 11 12	opsrtoslem1	$⊢ φ \to \underset{˙}{\leq} = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})$
45	44	difeq1d	$⊢ φ \to \underset{˙}{\leq} ∖ I = ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})) ∖ I$
46		relinxp	$⊢ Rel (\{⟨x, y⟩ \| ψ\} \cap (B \times B))$
47	46	a1i	$⊢ φ \to Rel (\{⟨x, y⟩ \| ψ\} \cap (B \times B))$
48		df-br	$⊢ a I b \leftrightarrow ⟨a, b⟩ \in I$
49		vex	$⊢ b \in V$
50	49	ideq	$⊢ a I b \leftrightarrow a = b$
51	48 50	bitr3i	$⊢ ⟨a, b⟩ \in I \leftrightarrow a = b$
52		brin	$⊢ a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \leftrightarrow (a \{⟨x, y⟩ \| ψ\} a \land a (B \times B) a)$
53	52	simprbi	$⊢ a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \to a (B \times B) a$
54		brxp	$⊢ a (B \times B) a \leftrightarrow (a \in B \land a \in B)$
55	54	simprbi	$⊢ a (B \times B) a \to a \in B$
56	53 55	syl	$⊢ a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \to a \in B$
57		sonr	$⊢ ((\{⟨x, y⟩ \| ψ\} \cap (B \times B)) Or B \land a \in B) \to \neg a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a$
58	57	ex	$⊢ (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) Or B \to (a \in B \to \neg a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a)$
59	32 56 58	syl2im	$⊢ φ \to (a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \to \neg a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a)$
60	59	pm2.01d	$⊢ φ \to \neg a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a$
61		breq2	$⊢ a = b \to (a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \leftrightarrow a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) b)$
62		df-br	$⊢ a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) b \leftrightarrow ⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B))$
63	61 62	syl6bb	$⊢ a = b \to (a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \leftrightarrow ⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B)))$
64	63	notbid	$⊢ a = b \to (\neg a (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) a \leftrightarrow \neg ⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B)))$
65	60 64	syl5ibcom	$⊢ φ \to (a = b \to \neg ⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B)))$
66	51 65	syl5bi	$⊢ φ \to (⟨a, b⟩ \in I \to \neg ⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B)))$
67	66	con2d	$⊢ φ \to (⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \to \neg ⟨a, b⟩ \in I)$
68		opex	$⊢ ⟨a, b⟩ \in V$
69		eldif	$⊢ ⟨a, b⟩ \in (V ∖ I) \leftrightarrow (⟨a, b⟩ \in V \land \neg ⟨a, b⟩ \in I)$
70	68 69	mpbiran	$⊢ ⟨a, b⟩ \in (V ∖ I) \leftrightarrow \neg ⟨a, b⟩ \in I$
71	67 70	syl6ibr	$⊢ φ \to (⟨a, b⟩ \in (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \to ⟨a, b⟩ \in (V ∖ I))$
72	47 71	relssdv	$⊢ φ \to \{⟨x, y⟩ \| ψ\} \cap (B \times B) \subseteq V ∖ I$
73		disj2	$⊢ (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cap I = \emptyset \leftrightarrow \{⟨x, y⟩ \| ψ\} \cap (B \times B) \subseteq V ∖ I$
74	72 73	sylibr	$⊢ φ \to (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cap I = \emptyset$
75		disj3	$⊢ (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cap I = \emptyset \leftrightarrow \{⟨x, y⟩ \| ψ\} \cap (B \times B) = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I$
76	74 75	sylib	$⊢ φ \to \{⟨x, y⟩ \| ψ\} \cap (B \times B) = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) ∖ I$
77	43 45 76	3eqtr4a	$⊢ φ \to \underset{˙}{\leq} ∖ I = \{⟨x, y⟩ \| ψ\} \cap (B \times B)$
78	36 77	syl5eq	$⊢ φ \to <_{O} = \{⟨x, y⟩ \| ψ\} \cap (B \times B)$
79		soeq1	$⊢ <_{O} = \{⟨x, y⟩ \| ψ\} \cap (B \times B) \to (<_{O} Or B \leftrightarrow (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) Or B)$
80	78 79	syl	$⊢ φ \to (<_{O} Or B \leftrightarrow (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) Or B)$
81	32 80	mpbird	$⊢ φ \to <_{O} Or B$
82	6 1 4	opsrbas	$⊢ φ \to {Base}_{S} = {Base}_{O}$
83	7 82	syl5eq	$⊢ φ \to B = {Base}_{O}$
84		soeq2	$⊢ B = {Base}_{O} \to (<_{O} Or B \leftrightarrow <_{O} Or {Base}_{O})$
85	83 84	syl	$⊢ φ \to (<_{O} Or B \leftrightarrow <_{O} Or {Base}_{O})$
86	81 85	mpbid	$⊢ φ \to <_{O} Or {Base}_{O}$
87	83	reseq2d	$⊢ φ \to {I ↾}_{B} = {I ↾}_{{Base}_{O}}$
88		ssun2	$⊢ {I ↾}_{B} \subseteq (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})$
89	87 88	eqsstrrdi	$⊢ φ \to {I ↾}_{{Base}_{O}} \subseteq (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})$
90	89 44	sseqtrrd	$⊢ φ \to {I ↾}_{{Base}_{O}} \subseteq \underset{˙}{\leq}$
91		eqid	$⊢ {Base}_{O} = {Base}_{O}$
92	91 12 34	tosso	$⊢ O \in V \to (O \in Toset \leftrightarrow (<_{O} Or {Base}_{O} \land {I ↾}_{{Base}_{O}} \subseteq \underset{˙}{\leq}))$
93	33 92	ax-mp	$⊢ O \in Toset \leftrightarrow (<_{O} Or {Base}_{O} \land {I ↾}_{{Base}_{O}} \subseteq \underset{˙}{\leq})$
94	86 90 93	sylanbrc	$⊢ φ \to O \in Toset$

Metamath Proof Explorer

Theorem opsrtoslem2

Proof