Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfpo2 Structured version   Visualization version   GIF version

Theorem dfpo2 30704
Description: Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.)
Assertion
Ref Expression
dfpo2 (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))

Proof of Theorem dfpo2
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 po0 4964 . . . 4 𝑅 Po ∅
2 res0 5308 . . . . . . 7 ( I ↾ ∅) = ∅
32ineq2i 3772 . . . . . 6 (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4 in0 3919 . . . . . 6 (𝑅 ∩ ∅) = ∅
53, 4eqtri 2631 . . . . 5 (𝑅 ∩ ( I ↾ ∅)) = ∅
6 xp0 5457 . . . . . . . . . 10 (𝐴 × ∅) = ∅
76ineq2i 3772 . . . . . . . . 9 (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
87, 4eqtri 2631 . . . . . . . 8 (𝑅 ∩ (𝐴 × ∅)) = ∅
98coeq2i 5192 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10 co02 5552 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
119, 10eqtri 2631 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12 0ss 3923 . . . . . 6 ∅ ⊆ 𝑅
1311, 12eqsstri 3597 . . . . 5 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
145, 13pm3.2i 469 . . . 4 ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
151, 142th 252 . . 3 (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16 poeq2 4953 . . . 4 (𝐴 = ∅ → (𝑅 Po 𝐴𝑅 Po ∅))
17 reseq2 5299 . . . . . . 7 (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
1817ineq2d 3775 . . . . . 6 (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
1918eqeq1d 2611 . . . . 5 (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20 xpeq2 5043 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
2120ineq2d 3775 . . . . . . 7 (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
2221coeq2d 5194 . . . . . 6 (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
2322sseq1d 3594 . . . . 5 (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
2419, 23anbi12d 742 . . . 4 (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
2516, 24bibi12d 333 . . 3 (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
2615, 25mpbiri 246 . 2 (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27 r19.28zv 4017 . . . . . . 7 (𝐴 ≠ ∅ → (∀𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2827ralbidv 2968 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29 r19.28zv 4017 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3028, 29bitrd 266 . . . . 5 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3130ralbidv 2968 . . . 4 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 r19.26 3045 . . . 4 (∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
3331, 32syl6bb 274 . . 3 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34 df-po 4949 . . 3 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35 disj 3968 . . . . 5 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36 df-ral 2900 . . . . 5 (∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37 opex 4853 . . . . . . . . . 10 𝑥, 𝑥⟩ ∈ V
38 eleq1 2675 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39 df-br 4578 . . . . . . . . . . . 12 (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
4038, 39syl6bbr 276 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅𝑥𝑅𝑥))
41 eleq1 2675 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42 vex 3175 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
43 ididg 5185 . . . . . . . . . . . . . . . 16 (𝑥 ∈ V → 𝑥 I 𝑥)
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15 𝑥 I 𝑥
4542brres 5310 . . . . . . . . . . . . . . 15 (𝑥( I ↾ 𝐴)𝑥 ↔ (𝑥 I 𝑥𝑥𝐴))
4644, 45mpbiran 954 . . . . . . . . . . . . . 14 (𝑥( I ↾ 𝐴)𝑥𝑥𝐴)
47 df-br 4578 . . . . . . . . . . . . . 14 (𝑥( I ↾ 𝐴)𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴))
4846, 47bitr3i 264 . . . . . . . . . . . . 13 (𝑥𝐴 ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴))
4941, 48syl6bbr 276 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
5049notbid 306 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥𝐴))
5140, 50imbi12d 332 . . . . . . . . . 10 (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥𝐴)))
5237, 51spcv 3271 . . . . . . . . 9 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥𝐴))
5352con2d 127 . . . . . . . 8 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝐴 → ¬ 𝑥𝑅𝑥))
5453alrimiv 1841 . . . . . . 7 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
55 relres 5333 . . . . . . . . . . . 12 Rel ( I ↾ 𝐴)
56 elrel 5134 . . . . . . . . . . . 12 ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5755, 56mpan 701 . . . . . . . . . . 11 (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5857ancri 572 . . . . . . . . . 10 (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
59 eleq1 2675 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
60 breq12 4582 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑅𝑥𝑦𝑅𝑦))
6160anidms 674 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑅𝑥𝑦𝑅𝑦))
6261notbid 306 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
6359, 62imbi12d 332 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑦)))
6463spv 2247 . . . . . . . . . . . . . 14 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦𝐴 → ¬ 𝑦𝑅𝑦))
65 breq2 4581 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → (𝑦𝑅𝑦𝑦𝑅𝑧))
6665notbid 306 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
6766imbi2d 328 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6867biimpcd 237 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6968impd 445 . . . . . . . . . . . . . 14 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦 = 𝑧𝑦𝐴) → ¬ 𝑦𝑅𝑧))
7064, 69syl 17 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦 = 𝑧𝑦𝐴) → ¬ 𝑦𝑅𝑧))
71 eleq1 2675 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
72 vex 3175 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
7372brres 5310 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦 I 𝑧𝑦𝐴))
74 df-br 4578 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7572ideq 5184 . . . . . . . . . . . . . . . . 17 (𝑦 I 𝑧𝑦 = 𝑧)
7675anbi1i 726 . . . . . . . . . . . . . . . 16 ((𝑦 I 𝑧𝑦𝐴) ↔ (𝑦 = 𝑧𝑦𝐴))
7773, 74, 763bitr3ri 289 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑧𝑦𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7871, 77syl6bbr 276 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦 = 𝑧𝑦𝐴)))
79 eleq1 2675 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
80 df-br 4578 . . . . . . . . . . . . . . . 16 (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
8179, 80syl6bbr 276 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅𝑦𝑅𝑧))
8281notbid 306 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤𝑅 ↔ ¬ 𝑦𝑅𝑧))
8378, 82imbi12d 332 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅) ↔ ((𝑦 = 𝑧𝑦𝐴) → ¬ 𝑦𝑅𝑧)))
8470, 83syl5ibrcom 235 . . . . . . . . . . . 12 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8584exlimdvv 1848 . . . . . . . . . . 11 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8685impd 445 . . . . . . . . . 10 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤𝑅))
8758, 86syl5 33 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅))
8887con2d 127 . . . . . . . 8 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8988alrimiv 1841 . . . . . . 7 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
9054, 89impbii 197 . . . . . 6 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
91 df-ral 2900 . . . . . 6 (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
9290, 91bitr4i 265 . . . . 5 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
9335, 36, 923bitri 284 . . . 4 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
94 ralcom 3078 . . . . . . 7 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
95 r19.23v 3004 . . . . . . . 8 (∀𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9695ralbii 2962 . . . . . . 7 (∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9794, 96bitri 262 . . . . . 6 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9897ralbii 2962 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
99 brin 4628 . . . . . . . . . . . 12 (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦))
100 brin 4628 . . . . . . . . . . . 12 (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧))
10199, 100anbi12i 728 . . . . . . . . . . 11 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)))
102 an4 860 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)))
103 ancom 464 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
104 ancom 464 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
105104anbi1i 726 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
106 brxp 5061 . . . . . . . . . . . . . . 15 (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥𝐴𝑦𝐴))
107 brxp 5061 . . . . . . . . . . . . . . 15 (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦𝐴𝑧𝐴))
108106, 107anbi12i 728 . . . . . . . . . . . . . 14 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)))
109 anandi 866 . . . . . . . . . . . . . 14 ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
110105, 108, 1093bitr4i 290 . . . . . . . . . . . . 13 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)))
111110anbi1i 726 . . . . . . . . . . . 12 (((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
112102, 103, 1113bitri 284 . . . . . . . . . . 11 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
113 anass 678 . . . . . . . . . . 11 (((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
114101, 112, 1133bitri 284 . . . . . . . . . 10 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
115114exbii 1763 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
11642, 72brco 5202 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
117 df-br 4578 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
118116, 117bitr3i 264 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119 df-rex 2901 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
120 r19.42v 3072 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
121119, 120bitr3i 264 . . . . . . . . 9 (∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
122115, 118, 1213bitr3ri 289 . . . . . . . 8 (((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
123 df-br 4578 . . . . . . . 8 (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
124122, 123imbi12i 338 . . . . . . 7 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
1251242albii 1737 . . . . . 6 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
126 r2al 2922 . . . . . . 7 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
127 impexp 460 . . . . . . . 8 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
1281272albii 1737 . . . . . . 7 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
129126, 128bitr4i 265 . . . . . 6 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
130 relco 5536 . . . . . . 7 Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
131 ssrel 5120 . . . . . . 7 (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
132130, 131ax-mp 5 . . . . . 6 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
133125, 129, 1323bitr4i 290 . . . . 5 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
13498, 133bitr2i 263 . . . 4 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
13593, 134anbi12i 728 . . 3 (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
13633, 34, 1353bitr4g 301 . 2 (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
13726, 136pm2.61ine 2864 1 (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1976  wne 2779  wral 2895  wrex 2896  Vcvv 3172  cin 3538  wss 3539  c0 3873  cop 4130   class class class wbr 4577   I cid 4938   Po wpo 4947   × cxp 5026  cres 5030  ccom 5032  Rel wrel 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-id 4943  df-po 4949  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-res 5040
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator