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

Theorem dfpo2 33116
 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 5454 . . . 4 𝑅 Po ∅
2 res0 5822 . . . . . . 7 ( I ↾ ∅) = ∅
32ineq2i 4136 . . . . . 6 (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4 in0 4299 . . . . . 6 (𝑅 ∩ ∅) = ∅
53, 4eqtri 2821 . . . . 5 (𝑅 ∩ ( I ↾ ∅)) = ∅
6 xp0 5982 . . . . . . . . . 10 (𝐴 × ∅) = ∅
76ineq2i 4136 . . . . . . . . 9 (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
87, 4eqtri 2821 . . . . . . . 8 (𝑅 ∩ (𝐴 × ∅)) = ∅
98coeq2i 5695 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10 co02 6080 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
119, 10eqtri 2821 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12 0ss 4304 . . . . . 6 ∅ ⊆ 𝑅
1311, 12eqsstri 3949 . . . . 5 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
145, 13pm3.2i 474 . . . 4 ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
151, 142th 267 . . 3 (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16 poeq2 5442 . . . 4 (𝐴 = ∅ → (𝑅 Po 𝐴𝑅 Po ∅))
17 reseq2 5813 . . . . . . 7 (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
1817ineq2d 4139 . . . . . 6 (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
1918eqeq1d 2800 . . . . 5 (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20 xpeq2 5540 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
2120ineq2d 4139 . . . . . . 7 (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
2221coeq2d 5697 . . . . . 6 (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
2322sseq1d 3946 . . . . 5 (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
2419, 23anbi12d 633 . . . 4 (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
2516, 24bibi12d 349 . . 3 (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
2615, 25mpbiri 261 . 2 (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27 r19.28zv 4404 . . . . . . 7 (𝐴 ≠ ∅ → (∀𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2827ralbidv 3162 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29 r19.28zv 4404 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3028, 29bitrd 282 . . . . 5 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3130ralbidv 3162 . . . 4 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 r19.26 3137 . . . 4 (∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
3331, 32syl6bb 290 . . 3 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34 df-po 5438 . . 3 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35 disj 4355 . . . . 5 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36 df-ral 3111 . . . . 5 (∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37 opex 5321 . . . . . . . . . 10 𝑥, 𝑥⟩ ∈ V
38 eleq1 2877 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39 df-br 5031 . . . . . . . . . . . 12 (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
4038, 39bitr4di 292 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅𝑥𝑅𝑥))
41 eleq1 2877 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42 opelidres 5830 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4342elv 3446 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴)
4441, 43syl6bb 290 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4544notbid 321 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥𝐴))
4640, 45imbi12d 348 . . . . . . . . . 10 (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥𝐴)))
4737, 46spcv 3554 . . . . . . . . 9 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥𝐴))
4847con2d 136 . . . . . . . 8 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝐴 → ¬ 𝑥𝑅𝑥))
4948alrimiv 1928 . . . . . . 7 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
50 relres 5847 . . . . . . . . . . . 12 Rel ( I ↾ 𝐴)
51 elrel 5635 . . . . . . . . . . . 12 ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5250, 51mpan 689 . . . . . . . . . . 11 (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5352ancri 553 . . . . . . . . . 10 (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54 eleq1 2877 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
55 breq12 5035 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑅𝑥𝑦𝑅𝑦))
5655anidms 570 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑅𝑥𝑦𝑅𝑦))
5756notbid 321 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
5854, 57imbi12d 348 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑦)))
5958spvv 2003 . . . . . . . . . . . . . 14 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦𝐴 → ¬ 𝑦𝑅𝑦))
60 breq2 5034 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → (𝑦𝑅𝑦𝑦𝑅𝑧))
6160notbid 321 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
6261imbi2d 344 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6362biimpcd 252 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6463impcomd 415 . . . . . . . . . . . . . 14 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
6559, 64syl 17 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66 eleq1 2877 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67 vex 3444 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6867brresi 5827 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦𝐴𝑦 I 𝑧))
69 df-br 5031 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7067ideq 5687 . . . . . . . . . . . . . . . . 17 (𝑦 I 𝑧𝑦 = 𝑧)
7170anbi2i 625 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑦 I 𝑧) ↔ (𝑦𝐴𝑦 = 𝑧))
7268, 69, 713bitr3ri 305 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7366, 72bitr4di 292 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦𝐴𝑦 = 𝑧)))
74 eleq1 2877 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75 df-br 5031 . . . . . . . . . . . . . . . 16 (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
7674, 75bitr4di 292 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅𝑦𝑅𝑧))
7776notbid 321 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤𝑅 ↔ ¬ 𝑦𝑅𝑧))
7873, 77imbi12d 348 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅) ↔ ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
7965, 78syl5ibrcom 250 . . . . . . . . . . . 12 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8079exlimdvv 1935 . . . . . . . . . . 11 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8180impd 414 . . . . . . . . . 10 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤𝑅))
8253, 81syl5 34 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅))
8382con2d 136 . . . . . . . 8 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8483alrimiv 1928 . . . . . . 7 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8549, 84impbii 212 . . . . . 6 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
86 df-ral 3111 . . . . . 6 (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
8785, 86bitr4i 281 . . . . 5 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
8835, 36, 873bitri 300 . . . 4 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
89 ralcom 3307 . . . . . . 7 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90 r19.23v 3238 . . . . . . . 8 (∀𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9190ralbii 3133 . . . . . . 7 (∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9289, 91bitri 278 . . . . . 6 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9392ralbii 3133 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94 brin 5082 . . . . . . . . . . . 12 (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦))
95 brin 5082 . . . . . . . . . . . 12 (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧))
9694, 95anbi12i 629 . . . . . . . . . . 11 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)))
97 an4 655 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)))
98 ancom 464 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
99 ancom 464 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
10099anbi1i 626 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
101 brxp 5565 . . . . . . . . . . . . . . 15 (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥𝐴𝑦𝐴))
102 brxp 5565 . . . . . . . . . . . . . . 15 (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦𝐴𝑧𝐴))
103101, 102anbi12i 629 . . . . . . . . . . . . . 14 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)))
104 anandi 675 . . . . . . . . . . . . . 14 ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
105100, 103, 1043bitr4i 306 . . . . . . . . . . . . 13 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)))
106105anbi1i 626 . . . . . . . . . . . 12 (((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
10797, 98, 1063bitri 300 . . . . . . . . . . 11 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
108 anass 472 . . . . . . . . . . 11 (((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
10996, 107, 1083bitri 300 . . . . . . . . . 10 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
110109exbii 1849 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
111 vex 3444 . . . . . . . . . . 11 𝑥 ∈ V
112111, 67brco 5705 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113 df-br 5031 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114112, 113bitr3i 280 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115 df-rex 3112 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
116 r19.42v 3303 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
117115, 116bitr3i 280 . . . . . . . . 9 (∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
118110, 114, 1173bitr3ri 305 . . . . . . . 8 (((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119 df-br 5031 . . . . . . . 8 (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120118, 119imbi12i 354 . . . . . . 7 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
1211202albii 1822 . . . . . 6 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122 r2al 3166 . . . . . . 7 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123 impexp 454 . . . . . . . 8 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
1241232albii 1822 . . . . . . 7 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125122, 124bitr4i 281 . . . . . 6 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126 relco 6064 . . . . . . 7 Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127 ssrel 5621 . . . . . . 7 (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128126, 127ax-mp 5 . . . . . 6 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129121, 125, 1283bitr4i 306 . . . . 5 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
13093, 129bitr2i 279 . . . 4 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
13188, 130anbi12i 629 . . 3 (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
13233, 34, 1313bitr4g 317 . 2 (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
13326, 132pm2.61ine 3070 1 (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ⟨cop 4531   class class class wbr 5030   I cid 5424   Po wpo 5436   × cxp 5517   ↾ cres 5521   ∘ ccom 5523  Rel wrel 5524 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-id 5425  df-po 5438  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-res 5531 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator