MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfpo2 Structured version   Visualization version   GIF version

Theorem dfpo2 6249
Description: Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
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 5563 . . . 4 𝑅 Po ∅
2 res0 5942 . . . . . . 7 ( I ↾ ∅) = ∅
32ineq2i 4170 . . . . . 6 (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4 in0 4352 . . . . . 6 (𝑅 ∩ ∅) = ∅
53, 4eqtri 2761 . . . . 5 (𝑅 ∩ ( I ↾ ∅)) = ∅
6 xp0 6111 . . . . . . . . . 10 (𝐴 × ∅) = ∅
76ineq2i 4170 . . . . . . . . 9 (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
87, 4eqtri 2761 . . . . . . . 8 (𝑅 ∩ (𝐴 × ∅)) = ∅
98coeq2i 5817 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10 co02 6213 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
119, 10eqtri 2761 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12 0ss 4357 . . . . . 6 ∅ ⊆ 𝑅
1311, 12eqsstri 3979 . . . . 5 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
145, 13pm3.2i 472 . . . 4 ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
151, 142th 264 . . 3 (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16 poeq2 5550 . . . 4 (𝐴 = ∅ → (𝑅 Po 𝐴𝑅 Po ∅))
17 reseq2 5933 . . . . . . 7 (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
1817ineq2d 4173 . . . . . 6 (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
1918eqeq1d 2735 . . . . 5 (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20 xpeq2 5655 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
2120ineq2d 4173 . . . . . . 7 (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
2221coeq2d 5819 . . . . . 6 (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
2322sseq1d 3976 . . . . 5 (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
2419, 23anbi12d 632 . . . 4 (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
2516, 24bibi12d 346 . . 3 (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
2615, 25mpbiri 258 . 2 (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27 r19.28zv 4459 . . . . . . 7 (𝐴 ≠ ∅ → (∀𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2827ralbidv 3171 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29 r19.28zv 4459 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3028, 29bitrd 279 . . . . 5 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3130ralbidv 3171 . . . 4 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 r19.26 3111 . . . 4 (∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
3331, 32bitrdi 287 . . 3 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34 df-po 5546 . . 3 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35 disj 4408 . . . . 5 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36 df-ral 3062 . . . . 5 (∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37 opex 5422 . . . . . . . . . 10 𝑥, 𝑥⟩ ∈ V
38 eleq1 2822 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39 df-br 5107 . . . . . . . . . . . 12 (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
4038, 39bitr4di 289 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅𝑥𝑅𝑥))
41 eleq1 2822 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42 opelidres 5950 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4342elv 3450 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴)
4441, 43bitrdi 287 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4544notbid 318 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥𝐴))
4640, 45imbi12d 345 . . . . . . . . . 10 (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥𝐴)))
4737, 46spcv 3563 . . . . . . . . 9 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥𝐴))
4847con2d 134 . . . . . . . 8 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝐴 → ¬ 𝑥𝑅𝑥))
4948alrimiv 1931 . . . . . . 7 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
50 relres 5967 . . . . . . . . . . . 12 Rel ( I ↾ 𝐴)
51 elrel 5755 . . . . . . . . . . . 12 ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5250, 51mpan 689 . . . . . . . . . . 11 (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5352ancri 551 . . . . . . . . . 10 (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54 eleq1 2822 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
55 breq12 5111 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑅𝑥𝑦𝑅𝑦))
5655anidms 568 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑅𝑥𝑦𝑅𝑦))
5756notbid 318 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
5854, 57imbi12d 345 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑦)))
5958spvv 2001 . . . . . . . . . . . . . 14 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦𝐴 → ¬ 𝑦𝑅𝑦))
60 breq2 5110 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → (𝑦𝑅𝑦𝑦𝑅𝑧))
6160notbid 318 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
6261imbi2d 341 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6362biimpcd 249 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6463impcomd 413 . . . . . . . . . . . . . 14 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
6559, 64syl 17 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67 vex 3448 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6867brresi 5947 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦𝐴𝑦 I 𝑧))
69 df-br 5107 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7067ideq 5809 . . . . . . . . . . . . . . . . 17 (𝑦 I 𝑧𝑦 = 𝑧)
7170anbi2i 624 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑦 I 𝑧) ↔ (𝑦𝐴𝑦 = 𝑧))
7268, 69, 713bitr3ri 302 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7366, 72bitr4di 289 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦𝐴𝑦 = 𝑧)))
74 eleq1 2822 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75 df-br 5107 . . . . . . . . . . . . . . . 16 (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
7674, 75bitr4di 289 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅𝑦𝑅𝑧))
7776notbid 318 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤𝑅 ↔ ¬ 𝑦𝑅𝑧))
7873, 77imbi12d 345 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅) ↔ ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
7965, 78syl5ibrcom 247 . . . . . . . . . . . 12 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8079exlimdvv 1938 . . . . . . . . . . 11 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8180impd 412 . . . . . . . . . 10 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤𝑅))
8253, 81syl5 34 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅))
8382con2d 134 . . . . . . . 8 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8483alrimiv 1931 . . . . . . 7 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8549, 84impbii 208 . . . . . 6 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
86 df-ral 3062 . . . . . 6 (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
8785, 86bitr4i 278 . . . . 5 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
8835, 36, 873bitri 297 . . . 4 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
89 ralcom 3271 . . . . . . 7 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90 r19.23v 3176 . . . . . . . 8 (∀𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9190ralbii 3093 . . . . . . 7 (∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9289, 91bitri 275 . . . . . 6 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9392ralbii 3093 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94 brin 5158 . . . . . . . . . . . 12 (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦))
95 brin 5158 . . . . . . . . . . . 12 (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧))
9694, 95anbi12i 628 . . . . . . . . . . 11 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)))
97 an4 655 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)))
98 ancom 462 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
99 ancom 462 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
10099anbi1i 625 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
101 brxp 5682 . . . . . . . . . . . . . . 15 (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥𝐴𝑦𝐴))
102 brxp 5682 . . . . . . . . . . . . . . 15 (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦𝐴𝑧𝐴))
103101, 102anbi12i 628 . . . . . . . . . . . . . 14 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)))
104 anandi 675 . . . . . . . . . . . . . 14 ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
105100, 103, 1043bitr4i 303 . . . . . . . . . . . . 13 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)))
106105anbi1i 625 . . . . . . . . . . . 12 (((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
10797, 98, 1063bitri 297 . . . . . . . . . . 11 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
108 anass 470 . . . . . . . . . . 11 (((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
10996, 107, 1083bitri 297 . . . . . . . . . 10 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
110109exbii 1851 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
111 vex 3448 . . . . . . . . . . 11 𝑥 ∈ V
112111, 67brco 5827 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113 df-br 5107 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114112, 113bitr3i 277 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115 df-rex 3071 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
116 r19.42v 3184 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
117115, 116bitr3i 277 . . . . . . . . 9 (∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
118110, 114, 1173bitr3ri 302 . . . . . . . 8 (((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119 df-br 5107 . . . . . . . 8 (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120118, 119imbi12i 351 . . . . . . 7 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
1211202albii 1823 . . . . . 6 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122 r2al 3188 . . . . . . 7 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123 impexp 452 . . . . . . . 8 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
1241232albii 1823 . . . . . . 7 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125122, 124bitr4i 278 . . . . . 6 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126 relco 6061 . . . . . . 7 Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127 ssrel 5739 . . . . . . 7 (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128126, 127ax-mp 5 . . . . . 6 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129121, 125, 1283bitr4i 303 . . . . 5 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
13093, 129bitr2i 276 . . . 4 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
13188, 130anbi12i 628 . . 3 (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
13233, 34, 1313bitr4g 314 . 2 (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
13326, 132pm2.61ine 3025 1 (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107  wne 2940  wral 3061  wrex 3070  Vcvv 3444  cin 3910  wss 3911  c0 4283  cop 4593   class class class wbr 5106   I cid 5531   Po wpo 5544   × cxp 5632  cres 5636  ccom 5638  Rel wrel 5639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-id 5532  df-po 5546  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-res 5646
This theorem is referenced by:  predpo  6278
  Copyright terms: Public domain W3C validator