Metamath Proof Explorer

Theorem dfpo2

Description: Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfpo2 ( 𝑅 Po 𝐴 ↔ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 po0 ⊢ 𝑅 Po ∅
2 res0 ⊢ ( I ↾ ∅ ) = ∅
3 2 ineq2i ⊢ ( 𝑅 ∩ ( I ↾ ∅ ) ) = ( 𝑅 ∩ ∅ )
4 in0 ⊢ ( 𝑅 ∩ ∅ ) = ∅
5 3 4 eqtri ⊢ ( 𝑅 ∩ ( I ↾ ∅ ) ) = ∅
6 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
7 6 ineq2i ⊢ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) = ( 𝑅 ∩ ∅ )
8 7 4 eqtri ⊢ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) = ∅
9 8 coeq2i ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) = ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ∅ )
10 co02 ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ∅ ) = ∅
11 9 10 eqtri ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) = ∅
12 0ss ⊢ ∅ ⊆ 𝑅
13 11 12 eqsstri ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) ⊆ 𝑅
14 5 13 pm3.2i ⊢ ( ( 𝑅 ∩ ( I ↾ ∅ ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) ⊆ 𝑅 )
15 1 14 2th ⊢ ( 𝑅 Po ∅ ↔ ( ( 𝑅 ∩ ( I ↾ ∅ ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) ⊆ 𝑅 ) )
16 poeq2 ⊢ ( 𝐴 = ∅ → ( 𝑅 Po 𝐴 ↔ 𝑅 Po ∅ ) )
17 reseq2 ⊢ ( 𝐴 = ∅ → ( I ↾ 𝐴 ) = ( I ↾ ∅ ) )
18 17 ineq2d ⊢ ( 𝐴 = ∅ → ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ( 𝑅 ∩ ( I ↾ ∅ ) ) )
19 18 eqeq1d ⊢ ( 𝐴 = ∅ → ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ↔ ( 𝑅 ∩ ( I ↾ ∅ ) ) = ∅ ) )
20 xpeq2 ⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ( 𝐴 × ∅ ) )
21 20 ineq2d ⊢ ( 𝐴 = ∅ → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( 𝑅 ∩ ( 𝐴 × ∅ ) ) )
22 21 coeq2d ⊢ ( 𝐴 = ∅ → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) )
23 22 sseq1d ⊢ ( 𝐴 = ∅ → ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ↔ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) ⊆ 𝑅 ) )
24 19 23 anbi12d ⊢ ( 𝐴 = ∅ → ( ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) ↔ ( ( 𝑅 ∩ ( I ↾ ∅ ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) ⊆ 𝑅 ) ) )
25 16 24 bibi12d ⊢ ( 𝐴 = ∅ → ( ( 𝑅 Po 𝐴 ↔ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) ) ↔ ( 𝑅 Po ∅ ↔ ( ( 𝑅 ∩ ( I ↾ ∅ ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × ∅ ) ) ) ⊆ 𝑅 ) ) ) )
26 15 25 mpbiri ⊢ ( 𝐴 = ∅ → ( 𝑅 Po 𝐴 ↔ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) ) )
27 r19.28zv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
28 27 ralbidv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
29 r19.28zv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
30 28 29 bitrd ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
31 30 ralbidv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
32 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
33 31 32 bitrdi ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
34 df-po ⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
35 disj ⊢ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ↔ ∀ 𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴 ) )
36 df-ral ⊢ ( ∀ 𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) )
37 opex ⊢ ⟨ 𝑥 , 𝑥 ⟩ ∈ V
38 eleq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑤 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 ) )
39 df-br ⊢ ( 𝑥 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 )
40 38 39 bitr4di ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑤 ∈ 𝑅 ↔ 𝑥 𝑅 𝑥 ) )
41 eleq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑤 ∈ ( I ↾ 𝐴 ) ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ ( I ↾ 𝐴 ) ) )
42 opelidres ⊢ ( 𝑥 ∈ V → ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ( I ↾ 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) )
43 42 elv ⊢ ( ⟨ 𝑥 , 𝑥 ⟩ ∈ ( I ↾ 𝐴 ) ↔ 𝑥 ∈ 𝐴 )
44 41 43 bitrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑤 ∈ ( I ↾ 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) )
45 44 notbid ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ → ( ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ↔ ¬ 𝑥 ∈ 𝐴 ) )
46 40 45 imbi12d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ → ( ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) ↔ ( 𝑥 𝑅 𝑥 → ¬ 𝑥 ∈ 𝐴 ) ) )
47 37 46 spcv ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) → ( 𝑥 𝑅 𝑥 → ¬ 𝑥 ∈ 𝐴 ) )
48 47 con2d ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) )
49 48 alrimiv ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) )
50 relres ⊢ Rel ( I ↾ 𝐴 )
51 elrel ⊢ ( ( Rel ( I ↾ 𝐴 ) ∧ 𝑤 ∈ ( I ↾ 𝐴 ) ) → ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ )
52 50 51 mpan ⊢ ( 𝑤 ∈ ( I ↾ 𝐴 ) → ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ )
53 52 ancri ⊢ ( 𝑤 ∈ ( I ↾ 𝐴 ) → ( ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴 ) ) )
54 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
55 breq12 ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 𝑅 𝑥 ↔ 𝑦 𝑅 𝑦 ) )
56 55 anidms ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑥 ↔ 𝑦 𝑅 𝑦 ) )
57 56 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑦 ) )
58 54 57 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑦 ) ) )
59 58 spvv ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑦 ) )
60 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑦 ↔ 𝑦 𝑅 𝑧 ) )
61 60 notbid ⊢ ( 𝑦 = 𝑧 → ( ¬ 𝑦 𝑅 𝑦 ↔ ¬ 𝑦 𝑅 𝑧 ) )
62 61 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑧 ) ) )
63 62 biimpcd ⊢ ( ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑦 ) → ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑧 ) ) )
64 63 impcomd ⊢ ( ( 𝑦 ∈ 𝐴 → ¬ 𝑦 𝑅 𝑦 ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧 ) → ¬ 𝑦 𝑅 𝑧 ) )
65 59 64 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧 ) → ¬ 𝑦 𝑅 𝑧 ) )
66 eleq1 ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑤 ∈ ( I ↾ 𝐴 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ 𝐴 ) ) )
67 vex ⊢ 𝑧 ∈ V
68 67 brresi ⊢ ( 𝑦 ( I ↾ 𝐴 ) 𝑧 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧 ) )
69 df-br ⊢ ( 𝑦 ( I ↾ 𝐴 ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ 𝐴 ) )
70 67 ideq ⊢ ( 𝑦 I 𝑧 ↔ 𝑦 = 𝑧 )
71 70 anbi2i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 I 𝑧 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧 ) )
72 68 69 71 3bitr3ri ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ 𝐴 ) )
73 66 72 bitr4di ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑤 ∈ ( I ↾ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧 ) ) )
74 eleq1 ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑤 ∈ 𝑅 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) )
75 df-br ⊢ ( 𝑦 𝑅 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 )
76 74 75 bitr4di ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑤 ∈ 𝑅 ↔ 𝑦 𝑅 𝑧 ) )
77 76 notbid ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( ¬ 𝑤 ∈ 𝑅 ↔ ¬ 𝑦 𝑅 𝑧 ) )
78 73 77 imbi12d ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑤 ∈ ( I ↾ 𝐴 ) → ¬ 𝑤 ∈ 𝑅 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 = 𝑧 ) → ¬ 𝑦 𝑅 𝑧 ) ) )
79 65 78 syl5ibrcom ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑤 ∈ ( I ↾ 𝐴 ) → ¬ 𝑤 ∈ 𝑅 ) ) )
80 79 exlimdvv ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑤 ∈ ( I ↾ 𝐴 ) → ¬ 𝑤 ∈ 𝑅 ) ) )
81 80 impd ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( ( ∃ 𝑦 ∃ 𝑧 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴 ) ) → ¬ 𝑤 ∈ 𝑅 ) )
82 53 81 syl5 ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( 𝑤 ∈ ( I ↾ 𝐴 ) → ¬ 𝑤 ∈ 𝑅 ) )
83 82 con2d ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) )
84 83 alrimiv ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) )
85 49 84 impbii ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) )
86 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 𝑅 𝑥 ) )
87 85 86 bitr4i ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
88 35 36 87 3bitri ⊢ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
89 ralcom ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
90 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
91 90 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
92 89 91 bitri ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
93 92 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
94 brin ⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ) )
95 brin ⊢ ( 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ↔ ( 𝑦 𝑅 𝑧 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) )
96 94 95 anbi12i ⊢ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ) ∧ ( 𝑦 𝑅 𝑧 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ) )
97 an4 ⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ) ∧ ( 𝑦 𝑅 𝑧 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ∧ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ) )
98 ancom ⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ∧ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ) ↔ ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
99 ancom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
100 99 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) )
101 brxp ⊢ ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
102 brxp ⊢ ( 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
103 101 102 anbi12i ⊢ ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) )
104 anandi ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) )
105 100 103 104 3bitr4i ⊢ ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) )
106 105 anbi1i ⊢ ( ( ( 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
107 97 98 106 3bitri ⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑥 ( 𝐴 × 𝐴 ) 𝑦 ) ∧ ( 𝑦 𝑅 𝑧 ∧ 𝑦 ( 𝐴 × 𝐴 ) 𝑧 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
108 anass ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ) )
109 96 107 108 3bitri ⊢ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ) )
110 109 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ) )
111 vex ⊢ 𝑥 ∈ V
112 111 67 brco ⊢ ( 𝑥 ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) 𝑧 ↔ ∃ 𝑦 ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
113 df-br ⊢ ( 𝑥 ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
114 112 113 bitr3i ⊢ ( ∃ 𝑦 ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
115 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ) )
116 r19.42v ⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
117 115 116 bitr3i ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) )
118 110 114 117 3bitr3ri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
119 df-br ⊢ ( 𝑥 𝑅 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 )
120 118 119 imbi12i ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) )
121 120 2albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) )
122 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
123 impexp ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
124 123 2albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
125 122 124 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 ) )
126 relco ⊢ Rel ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
127 ssrel ⊢ ( Rel ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) ) )
128 126 127 ax-mp ⊢ ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝑅 ) )
129 121 125 128 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 )
130 93 129 bitr2i ⊢ ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
131 88 130 anbi12i ⊢ ( ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
132 33 34 131 3bitr4g ⊢ ( 𝐴 ≠ ∅ → ( 𝑅 Po 𝐴 ↔ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) ) )
133 26 132 pm2.61ine ⊢ ( 𝑅 Po 𝐴 ↔ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) )