Theorem 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	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
	isso2i.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
Assertion	isso2i	⊢ 𝑅 Or 𝐴

Proof

Step	Hyp	Ref	Expression
1		isso2i.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
2		isso2i.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
3		equid	⊢ 𝑥 = 𝑥
4	3	orci	⊢ ( 𝑥 = 𝑥 ∨ 𝑥 𝑅 𝑥 )
5		nfv	⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 = 𝑥 ∨ 𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
6		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
7	6	anbi2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) )
8		equequ2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑥 ) )
9		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
10	8 9	orbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 = 𝑥 ∨ 𝑥 𝑅 𝑥 ) ) )
11		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑥 ) )
12	11	notbid	⊢ ( 𝑦 = 𝑥 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝑥 ) )
13	10 12	bibi12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝑥 = 𝑥 ∨ 𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) ) )
14	7 13	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 = 𝑥 ∨ 𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) ) ) )
15	1	con2bid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
16	5 14 15	chvarfv	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 = 𝑥 ∨ 𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
17	4 16	mpbii	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
18	17	anidms	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 )
19	15	biimprd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑦 → ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
20	19	orrd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
21		3orass	⊢ ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 ∨ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
22	20 21	sylibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
23	18 2 22	issoi	⊢ 𝑅 Or 𝐴