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

Metamath Proof Explorer

Theorem opsrtoslem2

Proof