opsrtoslem1

	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	opsrtoslem1	$⊢ φ \to \underset{˙}{\leq} = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})$

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	6 1 7 8 9 10 12 4	opsrle	$⊢ φ \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
14		unopab	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land ψ)\} \cup \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land x = y)\} = \{⟨x, y⟩ \| ((\{x, y\} \subseteq B \land ψ) \lor (\{x, y\} \subseteq B \land x = y))\}$
15		inopab	$⊢ \{⟨x, y⟩ \| ψ\} \cap \{⟨x, y⟩ \| (x \in B \land y \in B)\} = \{⟨x, y⟩ \| (ψ \land (x \in B \land y \in B))\}$
16		df-xp	$⊢ B \times B = \{⟨x, y⟩ \| (x \in B \land y \in B)\}$
17	16	ineq2i	$⊢ \{⟨x, y⟩ \| ψ\} \cap (B \times B) = \{⟨x, y⟩ \| ψ\} \cap \{⟨x, y⟩ \| (x \in B \land y \in B)\}$
18		vex	$⊢ x \in V$
19		vex	$⊢ y \in V$
20	18 19	prss	$⊢ (x \in B \land y \in B) \leftrightarrow \{x, y\} \subseteq B$
21	20	anbi1i	$⊢ ((x \in B \land y \in B) \land ψ) \leftrightarrow (\{x, y\} \subseteq B \land ψ)$
22		ancom	$⊢ ((x \in B \land y \in B) \land ψ) \leftrightarrow (ψ \land (x \in B \land y \in B))$
23	21 22	bitr3i	$⊢ (\{x, y\} \subseteq B \land ψ) \leftrightarrow (ψ \land (x \in B \land y \in B))$
24	23	opabbii	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land ψ)\} = \{⟨x, y⟩ \| (ψ \land (x \in B \land y \in B))\}$
25	15 17 24	3eqtr4i	$⊢ \{⟨x, y⟩ \| ψ\} \cap (B \times B) = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land ψ)\}$
26		opabresid	$⊢ {I ↾}_{B} = \{⟨x, y⟩ \| (x \in B \land y = x)\}$
27		equcom	$⊢ x = y \leftrightarrow y = x$
28	27	anbi2i	$⊢ (x \in B \land x = y) \leftrightarrow (x \in B \land y = x)$
29		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
30	29	biimpac	$⊢ (x \in B \land x = y) \to y \in B$
31	30	pm4.71i	$⊢ (x \in B \land x = y) \leftrightarrow ((x \in B \land x = y) \land y \in B)$
32	28 31	bitr3i	$⊢ (x \in B \land y = x) \leftrightarrow ((x \in B \land x = y) \land y \in B)$
33		an32	$⊢ ((x \in B \land x = y) \land y \in B) \leftrightarrow ((x \in B \land y \in B) \land x = y)$
34	20	anbi1i	$⊢ ((x \in B \land y \in B) \land x = y) \leftrightarrow (\{x, y\} \subseteq B \land x = y)$
35	32 33 34	3bitri	$⊢ (x \in B \land y = x) \leftrightarrow (\{x, y\} \subseteq B \land x = y)$
36	35	opabbii	$⊢ \{⟨x, y⟩ \| (x \in B \land y = x)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land x = y)\}$
37	26 36	eqtri	$⊢ {I ↾}_{B} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land x = y)\}$
38	25 37	uneq12i	$⊢ (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B}) = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land ψ)\} \cup \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land x = y)\}$
39	11	orbi1i	$⊢ (ψ \lor x = y) \leftrightarrow (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y)$
40	39	anbi2i	$⊢ (\{x, y\} \subseteq B \land (ψ \lor x = y)) \leftrightarrow (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))$
41		andi	$⊢ (\{x, y\} \subseteq B \land (ψ \lor x = y)) \leftrightarrow ((\{x, y\} \subseteq B \land ψ) \lor (\{x, y\} \subseteq B \land x = y))$
42	40 41	bitr3i	$⊢ (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y)) \leftrightarrow ((\{x, y\} \subseteq B \land ψ) \lor (\{x, y\} \subseteq B \land x = y))$
43	42	opabbii	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \{⟨x, y⟩ \| ((\{x, y\} \subseteq B \land ψ) \lor (\{x, y\} \subseteq B \land x = y))\}$
44	14 38 43	3eqtr4ri	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})$
45	13 44	syl6eq	$⊢ φ \to \underset{˙}{\leq} = (\{⟨x, y⟩ \| ψ\} \cap (B \times B)) \cup ({I ↾}_{B})$

Metamath Proof Explorer

Theorem opsrtoslem1

Proof