isso2i

Description: Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypotheses	isso2i.1	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow \neg (x = y \lor y R x))$
	isso2i.2	$⊢ (x \in A \land y \in A \land z \in A) \to ((x R y \land y R z) \to x R z)$
Assertion	isso2i	$⊢ R Or A$

Proof

Step	Hyp	Ref	Expression
1		isso2i.1	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow \neg (x = y \lor y R x))$
2		isso2i.2	$⊢ (x \in A \land y \in A \land z \in A) \to ((x R y \land y R z) \to x R z)$
3		equid	$⊢ x = x$
4	3	orci	$⊢ (x = x \lor x R x)$
5		nfv	$⊢ Ⅎ y ((x \in A \land x \in A) \to ((x = x \lor x R x) \leftrightarrow \neg x R x))$
6		eleq1w	$⊢ y = x \to (y \in A \leftrightarrow x \in A)$
7	6	anbi2d	$⊢ y = x \to ((x \in A \land y \in A) \leftrightarrow (x \in A \land x \in A))$
8		equequ2	$⊢ y = x \to (x = y \leftrightarrow x = x)$
9		breq1	$⊢ y = x \to (y R x \leftrightarrow x R x)$
10	8 9	orbi12d	$⊢ y = x \to ((x = y \lor y R x) \leftrightarrow (x = x \lor x R x))$
11		breq2	$⊢ y = x \to (x R y \leftrightarrow x R x)$
12	11	notbid	$⊢ y = x \to (\neg x R y \leftrightarrow \neg x R x)$
13	10 12	bibi12d	$⊢ y = x \to (((x = y \lor y R x) \leftrightarrow \neg x R y) \leftrightarrow ((x = x \lor x R x) \leftrightarrow \neg x R x))$
14	7 13	imbi12d	$⊢ y = x \to (((x \in A \land y \in A) \to ((x = y \lor y R x) \leftrightarrow \neg x R y)) \leftrightarrow ((x \in A \land x \in A) \to ((x = x \lor x R x) \leftrightarrow \neg x R x)))$
15	1	con2bid	$⊢ (x \in A \land y \in A) \to ((x = y \lor y R x) \leftrightarrow \neg x R y)$
16	5 14 15	chvarfv	$⊢ (x \in A \land x \in A) \to ((x = x \lor x R x) \leftrightarrow \neg x R x)$
17	4 16	mpbii	$⊢ (x \in A \land x \in A) \to \neg x R x$
18	17	anidms	$⊢ x \in A \to \neg x R x$
19	15	biimprd	$⊢ (x \in A \land y \in A) \to (\neg x R y \to (x = y \lor y R x))$
20	19	orrd	$⊢ (x \in A \land y \in A) \to (x R y \lor (x = y \lor y R x))$
21		3orass	$⊢ (x R y \lor x = y \lor y R x) \leftrightarrow (x R y \lor (x = y \lor y R x))$
22	20 21	sylibr	$⊢ (x \in A \land y \in A) \to (x R y \lor x = y \lor y R x)$
23	18 2 22	issoi	$⊢ R Or A$

Metamath Proof Explorer

Theorem isso2i

Proof