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 32111
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 5215 . . . 4 𝑅 Po ∅
2 res0 5571 . . . . . . 7 ( I ↾ ∅) = ∅
32ineq2i 3975 . . . . . 6 (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4 in0 4132 . . . . . 6 (𝑅 ∩ ∅) = ∅
53, 4eqtri 2787 . . . . 5 (𝑅 ∩ ( I ↾ ∅)) = ∅
6 xp0 5737 . . . . . . . . . 10 (𝐴 × ∅) = ∅
76ineq2i 3975 . . . . . . . . 9 (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
87, 4eqtri 2787 . . . . . . . 8 (𝑅 ∩ (𝐴 × ∅)) = ∅
98coeq2i 5453 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10 co02 5837 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
119, 10eqtri 2787 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12 0ss 4136 . . . . . 6 ∅ ⊆ 𝑅
1311, 12eqsstri 3797 . . . . 5 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
145, 13pm3.2i 462 . . . 4 ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
151, 142th 255 . . 3 (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16 poeq2 5204 . . . 4 (𝐴 = ∅ → (𝑅 Po 𝐴𝑅 Po ∅))
17 reseq2 5562 . . . . . . 7 (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
1817ineq2d 3978 . . . . . 6 (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
1918eqeq1d 2767 . . . . 5 (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20 xpeq2 5300 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
2120ineq2d 3978 . . . . . . 7 (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
2221coeq2d 5455 . . . . . 6 (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
2322sseq1d 3794 . . . . 5 (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
2419, 23anbi12d 624 . . . 4 (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
2516, 24bibi12d 336 . . 3 (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
2615, 25mpbiri 249 . 2 (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27 r19.28zv 4227 . . . . . . 7 (𝐴 ≠ ∅ → (∀𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2827ralbidv 3133 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29 r19.28zv 4227 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3028, 29bitrd 270 . . . . 5 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3130ralbidv 3133 . . . 4 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 r19.26 3211 . . . 4 (∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
3331, 32syl6bb 278 . . 3 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34 df-po 5200 . . 3 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35 disj 4180 . . . . 5 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36 df-ral 3060 . . . . 5 (∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37 opex 5090 . . . . . . . . . 10 𝑥, 𝑥⟩ ∈ V
38 eleq1 2832 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39 df-br 4812 . . . . . . . . . . . 12 (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
4038, 39syl6bbr 280 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅𝑥𝑅𝑥))
41 eleq1 2832 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42 opelidres 5586 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4342elv 3354 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴)
4441, 43syl6bb 278 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4544notbid 309 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥𝐴))
4640, 45imbi12d 335 . . . . . . . . . 10 (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥𝐴)))
4737, 46spcv 3452 . . . . . . . . 9 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥𝐴))
4847con2d 131 . . . . . . . 8 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝐴 → ¬ 𝑥𝑅𝑥))
4948alrimiv 2022 . . . . . . 7 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
50 relres 5603 . . . . . . . . . . . 12 Rel ( I ↾ 𝐴)
51 elrel 5393 . . . . . . . . . . . 12 ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5250, 51mpan 681 . . . . . . . . . . 11 (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5352ancri 545 . . . . . . . . . 10 (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54 eleq1 2832 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
55 breq12 4816 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑅𝑥𝑦𝑅𝑦))
5655anidms 562 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑅𝑥𝑦𝑅𝑦))
5756notbid 309 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
5854, 57imbi12d 335 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑦)))
5958spv 2366 . . . . . . . . . . . . . 14 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦𝐴 → ¬ 𝑦𝑅𝑦))
60 breq2 4815 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → (𝑦𝑅𝑦𝑦𝑅𝑧))
6160notbid 309 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
6261imbi2d 331 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6362biimpcd 240 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6463impcomd 399 . . . . . . . . . . . . . 14 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
6559, 64syl 17 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66 eleq1 2832 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67 vex 3353 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6867brresi 5576 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦𝐴𝑦 I 𝑧))
69 df-br 4812 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7067ideq 5445 . . . . . . . . . . . . . . . . 17 (𝑦 I 𝑧𝑦 = 𝑧)
7170anbi2i 616 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑦 I 𝑧) ↔ (𝑦𝐴𝑦 = 𝑧))
7268, 69, 713bitr3ri 293 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7366, 72syl6bbr 280 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦𝐴𝑦 = 𝑧)))
74 eleq1 2832 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75 df-br 4812 . . . . . . . . . . . . . . . 16 (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
7674, 75syl6bbr 280 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅𝑦𝑅𝑧))
7776notbid 309 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤𝑅 ↔ ¬ 𝑦𝑅𝑧))
7873, 77imbi12d 335 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅) ↔ ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
7965, 78syl5ibrcom 238 . . . . . . . . . . . 12 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8079exlimdvv 2029 . . . . . . . . . . 11 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8180impd 398 . . . . . . . . . 10 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤𝑅))
8253, 81syl5 34 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅))
8382con2d 131 . . . . . . . 8 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8483alrimiv 2022 . . . . . . 7 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8549, 84impbii 200 . . . . . 6 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
86 df-ral 3060 . . . . . 6 (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
8785, 86bitr4i 269 . . . . 5 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
8835, 36, 873bitri 288 . . . 4 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
89 ralcom 3245 . . . . . . 7 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90 r19.23v 3170 . . . . . . . 8 (∀𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9190ralbii 3127 . . . . . . 7 (∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9289, 91bitri 266 . . . . . 6 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9392ralbii 3127 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94 brin 4863 . . . . . . . . . . . 12 (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦))
95 brin 4863 . . . . . . . . . . . 12 (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧))
9694, 95anbi12i 620 . . . . . . . . . . 11 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)))
97 an4 646 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)))
98 ancom 452 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
99 ancom 452 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
10099anbi1i 617 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
101 brxp 5325 . . . . . . . . . . . . . . 15 (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥𝐴𝑦𝐴))
102 brxp 5325 . . . . . . . . . . . . . . 15 (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦𝐴𝑧𝐴))
103101, 102anbi12i 620 . . . . . . . . . . . . . 14 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)))
104 anandi 666 . . . . . . . . . . . . . 14 ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
105100, 103, 1043bitr4i 294 . . . . . . . . . . . . 13 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)))
106105anbi1i 617 . . . . . . . . . . . 12 (((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
10797, 98, 1063bitri 288 . . . . . . . . . . 11 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
108 anass 460 . . . . . . . . . . 11 (((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
10996, 107, 1083bitri 288 . . . . . . . . . 10 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
110109exbii 1943 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
111 vex 3353 . . . . . . . . . . 11 𝑥 ∈ V
112111, 67brco 5463 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113 df-br 4812 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114112, 113bitr3i 268 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115 df-rex 3061 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
116 r19.42v 3239 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
117115, 116bitr3i 268 . . . . . . . . 9 (∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
118110, 114, 1173bitr3ri 293 . . . . . . . 8 (((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119 df-br 4812 . . . . . . . 8 (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120118, 119imbi12i 341 . . . . . . 7 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
1211202albii 1915 . . . . . 6 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122 r2al 3086 . . . . . . 7 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123 impexp 441 . . . . . . . 8 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
1241232albii 1915 . . . . . . 7 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125122, 124bitr4i 269 . . . . . 6 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126 relco 5821 . . . . . . 7 Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127 ssrel 5379 . . . . . . 7 (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128126, 127ax-mp 5 . . . . . 6 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129121, 125, 1283bitr4i 294 . . . . 5 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
13093, 129bitr2i 267 . . . 4 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
13188, 130anbi12i 620 . . 3 (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
13233, 34, 1313bitr4g 305 . 2 (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
13326, 132pm2.61ine 3020 1 (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1650   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  cin 3733  wss 3734  c0 4081  cop 4342   class class class wbr 4811   I cid 5186   Po wpo 5198   × cxp 5277  cres 5281  ccom 5283  Rel wrel 5284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-id 5187  df-po 5200  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-res 5291
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator