ltsval2

Description: Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011)

		Ref	Expression
	Assertion	ltsval2	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$

Proof

Step	Hyp	Ref	Expression
1		ltsval	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
2		fvex	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \in V$
3		fvex	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) \in V$
4	2 3	brtp	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \leftrightarrow ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
5		1n0	$⊢ 1_{𝑜} \neq \emptyset$
6	5	neii	$⊢ \neg 1_{𝑜} = \emptyset$
7		eqeq1	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \leftrightarrow 1_{𝑜} = \emptyset)$
8	6 7	mtbiri	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \to \neg A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
9		fvprc	$⊢ \neg ⋂ \{a \in On \| A (a) \neq B (a)\} \in V \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
10	8 9	nsyl2	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
11	10	adantr	$⊢ (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
12	10	adantr	$⊢ (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
13		2on0	$⊢ 2_{𝑜} \neq \emptyset$
14	13	neii	$⊢ \neg 2_{𝑜} = \emptyset$
15		eqeq1	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜} \to (B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \leftrightarrow 2_{𝑜} = \emptyset)$
16	14 15	mtbiri	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜} \to \neg B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
17		fvprc	$⊢ \neg ⋂ \{a \in On \| A (a) \neq B (a)\} \in V \to B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
18	16 17	nsyl2	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜} \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
19	18	adantl	$⊢ (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
20	11 12 19	3jaoi	$⊢ ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
21	4 20	sylbi	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in V$
22		onintrab	$⊢ ⋂ \{a \in On \| A (a) \neq B (a)\} \in V \leftrightarrow ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
23	21 22	sylib	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
24	23	adantl	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
25		onelon	$⊢ (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land y \in ⋂ \{a \in On \| A (a) \neq B (a)\}) \to y \in On$
26	25	expcom	$⊢ y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \to y \in On)$
27	24 26	syl5	$⊢ y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to (((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to y \in On)$
28		fveq2	$⊢ a = y \to A (a) = A (y)$
29		fveq2	$⊢ a = y \to B (a) = B (y)$
30	28 29	neeq12d	$⊢ a = y \to (A (a) \neq B (a) \leftrightarrow A (y) \neq B (y))$
31	30	onnminsb	$⊢ y \in On \to (y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to \neg A (y) \neq B (y))$
32	31	com12	$⊢ y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to (y \in On \to \neg A (y) \neq B (y))$
33	27 32	syldc	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to (y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to \neg A (y) \neq B (y))$
34		df-ne	$⊢ A (y) \neq B (y) \leftrightarrow \neg A (y) = B (y)$
35	34	con2bii	$⊢ A (y) = B (y) \leftrightarrow \neg A (y) \neq B (y)$
36	33 35	imbitrrdi	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to (y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (y) = B (y))$
37	36	ralrimiv	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y)$
38	24 37	jca	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y))$
39	38	ex	$⊢ (A \in No \land B \in No) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y)))$
40	39	impac	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to ((⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y)) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
41		anass	$⊢ ((⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y)) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \leftrightarrow (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})))$
42	40 41	sylib	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})))$
43		raleq	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (\forall y \in x A (y) = B (y) \leftrightarrow \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y))$
44		fveq2	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (x) = A (⋂ \{a \in On \| A (a) \neq B (a)\})$
45		fveq2	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to B (x) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
46	44 45	breq12d	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
47	43 46	anbi12d	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to ((\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})))$
48	47	rspcev	$⊢ (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = B (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))) \to \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
49	42 48	syl	$⊢ ((A \in No \land B \in No) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})) \to \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
50	49	ex	$⊢ (A \in No \land B \in No) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \to \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
51		eqeq12	$⊢ (A (x) = 1_{𝑜} \land B (x) = \emptyset) \to (A (x) = B (x) \leftrightarrow 1_{𝑜} = \emptyset)$
52	6 51	mtbiri	$⊢ (A (x) = 1_{𝑜} \land B (x) = \emptyset) \to \neg A (x) = B (x)$
53		1on	$⊢ 1_{𝑜} \in On$
54		0elon	$⊢ \emptyset \in On$
55		suc11	$⊢ (1_{𝑜} \in On \land \emptyset \in On) \to (suc 1_{𝑜} = suc \emptyset \leftrightarrow 1_{𝑜} = \emptyset)$
56	55	necon3bid	$⊢ (1_{𝑜} \in On \land \emptyset \in On) \to (suc 1_{𝑜} \neq suc \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset)$
57	53 54 56	mp2an	$⊢ suc 1_{𝑜} \neq suc \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset$
58	5 57	mpbir	$⊢ suc 1_{𝑜} \neq suc \emptyset$
59		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
60		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
61	59 60	eqeq12i	$⊢ 2_{𝑜} = 1_{𝑜} \leftrightarrow suc 1_{𝑜} = suc \emptyset$
62	58 61	nemtbir	$⊢ \neg 2_{𝑜} = 1_{𝑜}$
63		eqeq12	$⊢ (A (x) = 1_{𝑜} \land B (x) = 2_{𝑜}) \to (A (x) = B (x) \leftrightarrow 1_{𝑜} = 2_{𝑜})$
64		eqcom	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow 2_{𝑜} = 1_{𝑜}$
65	63 64	bitrdi	$⊢ (A (x) = 1_{𝑜} \land B (x) = 2_{𝑜}) \to (A (x) = B (x) \leftrightarrow 2_{𝑜} = 1_{𝑜})$
66	62 65	mtbiri	$⊢ (A (x) = 1_{𝑜} \land B (x) = 2_{𝑜}) \to \neg A (x) = B (x)$
67	13	nesymi	$⊢ \neg \emptyset = 2_{𝑜}$
68		eqeq12	$⊢ (A (x) = \emptyset \land B (x) = 2_{𝑜}) \to (A (x) = B (x) \leftrightarrow \emptyset = 2_{𝑜})$
69	67 68	mtbiri	$⊢ (A (x) = \emptyset \land B (x) = 2_{𝑜}) \to \neg A (x) = B (x)$
70	52 66 69	3jaoi	$⊢ ((A (x) = 1_{𝑜} \land B (x) = \emptyset) \lor (A (x) = 1_{𝑜} \land B (x) = 2_{𝑜}) \lor (A (x) = \emptyset \land B (x) = 2_{𝑜})) \to \neg A (x) = B (x)$
71		fvex	$⊢ A (x) \in V$
72		fvex	$⊢ B (x) \in V$
73	71 72	brtp	$⊢ A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \leftrightarrow ((A (x) = 1_{𝑜} \land B (x) = \emptyset) \lor (A (x) = 1_{𝑜} \land B (x) = 2_{𝑜}) \lor (A (x) = \emptyset \land B (x) = 2_{𝑜}))$
74		df-ne	$⊢ A (x) \neq B (x) \leftrightarrow \neg A (x) = B (x)$
75	70 73 74	3imtr4i	$⊢ A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \to A (x) \neq B (x)$
76		fveq2	$⊢ a = x \to A (a) = A (x)$
77		fveq2	$⊢ a = x \to B (a) = B (x)$
78	76 77	neeq12d	$⊢ a = x \to (A (a) \neq B (a) \leftrightarrow A (x) \neq B (x))$
79	78	elrab	$⊢ x \in \{a \in On \| A (a) \neq B (a)\} \leftrightarrow (x \in On \land A (x) \neq B (x))$
80	79	biimpri	$⊢ (x \in On \land A (x) \neq B (x)) \to x \in \{a \in On \| A (a) \neq B (a)\}$
81	80	adantlr	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \neq B (x)) \to x \in \{a \in On \| A (a) \neq B (a)\}$
82		ssrab2	$⊢ \{a \in On \| A (a) \neq B (a)\} \subseteq On$
83		ne0i	$⊢ x \in \{a \in On \| A (a) \neq B (a)\} \to \{a \in On \| A (a) \neq B (a)\} \neq \emptyset$
84	83	adantl	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to \{a \in On \| A (a) \neq B (a)\} \neq \emptyset$
85		onint	$⊢ (\{a \in On \| A (a) \neq B (a)\} \subseteq On \land \{a \in On \| A (a) \neq B (a)\} \neq \emptyset) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in \{a \in On \| A (a) \neq B (a)\}$
86	82 84 85	sylancr	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in \{a \in On \| A (a) \neq B (a)\}$
87		nfrab1	$⊢ \underline{Ⅎ} a \{a \in On \| A (a) \neq B (a)\}$
88	87	nfint	$⊢ \underline{Ⅎ} a ⋂ \{a \in On \| A (a) \neq B (a)\}$
89		nfcv	$⊢ \underline{Ⅎ} a On$
90		nfcv	$⊢ \underline{Ⅎ} a A$
91	90 88	nffv	$⊢ \underline{Ⅎ} a A (⋂ \{a \in On \| A (a) \neq B (a)\})$
92		nfcv	$⊢ \underline{Ⅎ} a B$
93	92 88	nffv	$⊢ \underline{Ⅎ} a B (⋂ \{a \in On \| A (a) \neq B (a)\})$
94	91 93	nfne	$⊢ Ⅎ a A (⋂ \{a \in On \| A (a) \neq B (a)\}) \neq B (⋂ \{a \in On \| A (a) \neq B (a)\})$
95		fveq2	$⊢ a = ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (a) = A (⋂ \{a \in On \| A (a) \neq B (a)\})$
96		fveq2	$⊢ a = ⋂ \{a \in On \| A (a) \neq B (a)\} \to B (a) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
97	95 96	neeq12d	$⊢ a = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (A (a) \neq B (a) \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \neq B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
98	88 89 94 97	elrabf	$⊢ ⋂ \{a \in On \| A (a) \neq B (a)\} \in \{a \in On \| A (a) \neq B (a)\} \leftrightarrow (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \neq B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
99	98	simprbi	$⊢ ⋂ \{a \in On \| A (a) \neq B (a)\} \in \{a \in On \| A (a) \neq B (a)\} \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \neq B (⋂ \{a \in On \| A (a) \neq B (a)\})$
100	86 99	syl	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \neq B (⋂ \{a \in On \| A (a) \neq B (a)\})$
101		df-ne	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \neq B (⋂ \{a \in On \| A (a) \neq B (a)\}) \leftrightarrow \neg A (⋂ \{a \in On \| A (a) \neq B (a)\}) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
102	100 101	sylib	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to \neg A (⋂ \{a \in On \| A (a) \neq B (a)\}) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
103		fveq2	$⊢ y = ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (y) = A (⋂ \{a \in On \| A (a) \neq B (a)\})$
104		fveq2	$⊢ y = ⋂ \{a \in On \| A (a) \neq B (a)\} \to B (y) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
105	103 104	eqeq12d	$⊢ y = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (A (y) = B (y) \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) = B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
106	105	rspccv	$⊢ \forall y \in x A (y) = B (y) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in x \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) = B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
107	106	ad2antlr	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to (⋂ \{a \in On \| A (a) \neq B (a)\} \in x \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) = B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
108	102 107	mtod	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to \neg ⋂ \{a \in On \| A (a) \neq B (a)\} \in x$
109		simpll	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to x \in On$
110		oninton	$⊢ (\{a \in On \| A (a) \neq B (a)\} \subseteq On \land \{a \in On \| A (a) \neq B (a)\} \neq \emptyset) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
111	82 83 110	sylancr	$⊢ x \in \{a \in On \| A (a) \neq B (a)\} \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
112	111	adantl	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
113		ontri1	$⊢ (x \in On \land ⋂ \{a \in On \| A (a) \neq B (a)\} \in On) \to (x \subseteq ⋂ \{a \in On \| A (a) \neq B (a)\} \leftrightarrow \neg ⋂ \{a \in On \| A (a) \neq B (a)\} \in x)$
114	109 112 113	syl2anc	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to (x \subseteq ⋂ \{a \in On \| A (a) \neq B (a)\} \leftrightarrow \neg ⋂ \{a \in On \| A (a) \neq B (a)\} \in x)$
115	108 114	mpbird	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to x \subseteq ⋂ \{a \in On \| A (a) \neq B (a)\}$
116		intss1	$⊢ x \in \{a \in On \| A (a) \neq B (a)\} \to ⋂ \{a \in On \| A (a) \neq B (a)\} \subseteq x$
117	116	adantl	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \subseteq x$
118	115 117	eqssd	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land x \in \{a \in On \| A (a) \neq B (a)\}) \to x = ⋂ \{a \in On \| A (a) \neq B (a)\}$
119	81 118	syldan	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \neq B (x)) \to x = ⋂ \{a \in On \| A (a) \neq B (a)\}$
120	75 119	sylan2	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to x = ⋂ \{a \in On \| A (a) \neq B (a)\}$
121	120	fveq2d	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to A (x) = A (⋂ \{a \in On \| A (a) \neq B (a)\})$
122	120	fveq2d	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to B (x) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
123	121 122	breq12d	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
124	123	biimpd	$⊢ ((x \in On \land \forall y \in x A (y) = B (y)) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
125	124	ex	$⊢ (x \in On \land \forall y \in x A (y) = B (y)) \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})))$
126	125	pm2.43d	$⊢ (x \in On \land \forall y \in x A (y) = B (y)) \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
127	126	expimpd	$⊢ x \in On \to ((\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
128	127	rexlimiv	$⊢ \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})$
129	50 128	impbid1	$⊢ (A \in No \land B \in No) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \leftrightarrow \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
130	1 129	bitr4d	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$

Metamath Proof Explorer

Theorem ltsval2

Proof