Theorem asymref

Description: Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld . (Contributed by NM, 6-May-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	asymref	⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ ∪ ∪ 𝑅 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	opeluu	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑦 ∈ ∪ ∪ 𝑅 ) )
5	1 4	sylbi	⊢ ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑦 ∈ ∪ ∪ 𝑅 ) )
6	5	simpld	⊢ ( 𝑥 𝑅 𝑦 → 𝑥 ∈ ∪ ∪ 𝑅 )
7	6	adantr	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 ∈ ∪ ∪ 𝑅 )
8	7	pm4.71ri	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
9	8	bibi1i	⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) )
10		elin	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 ) )
11	2 3	brcnv	⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
12		df-br	⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 )
13	11 12	bitr3i	⊢ ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 )
14	1 13	anbi12i	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 ) )
15	10 14	bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) )
16	3	opelresi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
17		df-br	⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
18	3	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
19	17 18	bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑥 = 𝑦 )
20	19	anbi2i	⊢ ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) )
21	16 20	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) )
22	15 21	bibi12i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) )
23		pm5.32	⊢ ( ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) )
24	9 22 23	3bitr4i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
25	24	albii	⊢ ( ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ∀ 𝑦 ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
26		19.21v	⊢ ( ∀ 𝑦 ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
27	25 26	bitri	⊢ ( ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
28	27	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
29		relcnv	⊢ Rel ◡ 𝑅
30		relin2	⊢ ( Rel ◡ 𝑅 → Rel ( 𝑅 ∩ ◡ 𝑅 ) )
31	29 30	ax-mp	⊢ Rel ( 𝑅 ∩ ◡ 𝑅 )
32		relres	⊢ Rel ( I ↾ ∪ ∪ 𝑅 )
33		eqrel	⊢ ( ( Rel ( 𝑅 ∩ ◡ 𝑅 ) ∧ Rel ( I ↾ ∪ ∪ 𝑅 ) ) → ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ) )
34	31 32 33	mp2an	⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) )
35		df-ral	⊢ ( ∀ 𝑥 ∈ ∪ ∪ 𝑅 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
36	28 34 35	3bitr4i	⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ ∪ ∪ 𝑅 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) )