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 33441
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 5485 . . . 4 𝑅 Po ∅
2 res0 5855 . . . . . . 7 ( I ↾ ∅) = ∅
32ineq2i 4124 . . . . . 6 (𝑅 ∩ ( I ↾ ∅)) = (𝑅 ∩ ∅)
4 in0 4306 . . . . . 6 (𝑅 ∩ ∅) = ∅
53, 4eqtri 2765 . . . . 5 (𝑅 ∩ ( I ↾ ∅)) = ∅
6 xp0 6021 . . . . . . . . . 10 (𝐴 × ∅) = ∅
76ineq2i 4124 . . . . . . . . 9 (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅)
87, 4eqtri 2765 . . . . . . . 8 (𝑅 ∩ (𝐴 × ∅)) = ∅
98coeq2i 5729 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅)
10 co02 6124 . . . . . . 7 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) = ∅
119, 10eqtri 2765 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ∅
12 0ss 4311 . . . . . 6 ∅ ⊆ 𝑅
1311, 12eqsstri 3935 . . . . 5 ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅
145, 13pm3.2i 474 . . . 4 ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)
151, 142th 267 . . 3 (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
16 poeq2 5472 . . . 4 (𝐴 = ∅ → (𝑅 Po 𝐴𝑅 Po ∅))
17 reseq2 5846 . . . . . . 7 (𝐴 = ∅ → ( I ↾ 𝐴) = ( I ↾ ∅))
1817ineq2d 4127 . . . . . 6 (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾ ∅)))
1918eqeq1d 2739 . . . . 5 (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) = ∅))
20 xpeq2 5572 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅))
2120ineq2d 4127 . . . . . . 7 (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅)))
2221coeq2d 5731 . . . . . 6 (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))))
2322sseq1d 3932 . . . . 5 (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))
2419, 23anbi12d 634 . . . 4 (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))
2516, 24bibi12d 349 . . 3 (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))))
2615, 25mpbiri 261 . 2 (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
27 r19.28zv 4412 . . . . . . 7 (𝐴 ≠ ∅ → (∀𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2827ralbidv 3118 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
29 r19.28zv 4412 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑥𝑅𝑥 ∧ ∀𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3028, 29bitrd 282 . . . . 5 (𝐴 ≠ ∅ → (∀𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3130ralbidv 3118 . . . 4 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 r19.26 3092 . . . 4 (∀𝑥𝐴𝑥𝑅𝑥 ∧ ∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
3331, 32bitrdi 290 . . 3 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
34 df-po 5468 . . 3 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
35 disj 4362 . . . . 5 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴))
36 df-ral 3066 . . . . 5 (∀𝑤𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
37 opex 5348 . . . . . . . . . 10 𝑥, 𝑥⟩ ∈ V
38 eleq1 2825 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅))
39 df-br 5054 . . . . . . . . . . . 12 (𝑥𝑅𝑥 ↔ ⟨𝑥, 𝑥⟩ ∈ 𝑅)
4038, 39bitr4di 292 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤𝑅𝑥𝑅𝑥))
41 eleq1 2825 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴)))
42 opelidres 5863 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4342elv 3414 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴)
4441, 43bitrdi 290 . . . . . . . . . . . 12 (𝑤 = ⟨𝑥, 𝑥⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥𝐴))
4544notbid 321 . . . . . . . . . . 11 (𝑤 = ⟨𝑥, 𝑥⟩ → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥𝐴))
4640, 45imbi12d 348 . . . . . . . . . 10 (𝑤 = ⟨𝑥, 𝑥⟩ → ((𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥𝐴)))
4737, 46spcv 3520 . . . . . . . . 9 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥𝐴))
4847con2d 136 . . . . . . . 8 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝐴 → ¬ 𝑥𝑅𝑥))
4948alrimiv 1935 . . . . . . 7 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
50 relres 5880 . . . . . . . . . . . 12 Rel ( I ↾ 𝐴)
51 elrel 5668 . . . . . . . . . . . 12 ((Rel ( I ↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5250, 51mpan 690 . . . . . . . . . . 11 (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩)
5352ancri 553 . . . . . . . . . 10 (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)))
54 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
55 breq12 5058 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑅𝑥𝑦𝑅𝑦))
5655anidms 570 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑥𝑅𝑥𝑦𝑅𝑦))
5756notbid 321 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦))
5854, 57imbi12d 348 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑥𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑦)))
5958spvv 2005 . . . . . . . . . . . . . 14 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦𝐴 → ¬ 𝑦𝑅𝑦))
60 breq2 5057 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → (𝑦𝑅𝑦𝑦𝑅𝑧))
6160notbid 321 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧))
6261imbi2d 344 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6362biimpcd 252 . . . . . . . . . . . . . . 15 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦𝐴 → ¬ 𝑦𝑅𝑧)))
6463impcomd 415 . . . . . . . . . . . . . 14 ((𝑦𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
6559, 64syl 17 . . . . . . . . . . . . 13 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧))
66 eleq1 2825 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴)))
67 vex 3412 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6867brresi 5860 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦𝐴𝑦 I 𝑧))
69 df-br 5054 . . . . . . . . . . . . . . . 16 (𝑦( I ↾ 𝐴)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7067ideq 5721 . . . . . . . . . . . . . . . . 17 (𝑦 I 𝑧𝑦 = 𝑧)
7170anbi2i 626 . . . . . . . . . . . . . . . 16 ((𝑦𝐴𝑦 I 𝑧) ↔ (𝑦𝐴𝑦 = 𝑧))
7268, 69, 713bitr3ri 305 . . . . . . . . . . . . . . 15 ((𝑦𝐴𝑦 = 𝑧) ↔ ⟨𝑦, 𝑧⟩ ∈ ( I ↾ 𝐴))
7366, 72bitr4di 292 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦𝐴𝑦 = 𝑧)))
74 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
75 df-br 5054 . . . . . . . . . . . . . . . 16 (𝑦𝑅𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅)
7674, 75bitr4di 292 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤𝑅𝑦𝑅𝑧))
7776notbid 321 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑦, 𝑧⟩ → (¬ 𝑤𝑅 ↔ ¬ 𝑦𝑅𝑧))
7873, 77imbi12d 348 . . . . . . . . . . . . 13 (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅) ↔ ((𝑦𝐴𝑦 = 𝑧) → ¬ 𝑦𝑅𝑧)))
7965, 78syl5ibrcom 250 . . . . . . . . . . . 12 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8079exlimdvv 1942 . . . . . . . . . . 11 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅)))
8180impd 414 . . . . . . . . . 10 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦𝑧 𝑤 = ⟨𝑦, 𝑧⟩ ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤𝑅))
8253, 81syl5 34 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤𝑅))
8382con2d 136 . . . . . . . 8 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8483alrimiv 1935 . . . . . . 7 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)))
8549, 84impbii 212 . . . . . 6 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
86 df-ral 3066 . . . . . 6 (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝑅𝑥))
8785, 86bitr4i 281 . . . . 5 (∀𝑤(𝑤𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
8835, 36, 873bitri 300 . . . 4 ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥)
89 ralcom 3267 . . . . . . 7 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
90 r19.23v 3198 . . . . . . . 8 (∀𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9190ralbii 3088 . . . . . . 7 (∀𝑧𝐴𝑦𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9289, 91bitri 278 . . . . . 6 (∀𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
9392ralbii 3088 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
94 brin 5105 . . . . . . . . . . . 12 (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦))
95 brin 5105 . . . . . . . . . . . 12 (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧))
9694, 95anbi12i 630 . . . . . . . . . . 11 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)))
97 an4 656 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)))
98 ancom 464 . . . . . . . . . . . 12 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
99 ancom 464 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
10099anbi1i 627 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
101 brxp 5598 . . . . . . . . . . . . . . 15 (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥𝐴𝑦𝐴))
102 brxp 5598 . . . . . . . . . . . . . . 15 (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦𝐴𝑧𝐴))
103101, 102anbi12i 630 . . . . . . . . . . . . . 14 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑦𝐴𝑧𝐴)))
104 anandi 676 . . . . . . . . . . . . . 14 ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝑦𝐴𝑧𝐴)))
105100, 103, 1043bitr4i 306 . . . . . . . . . . . . 13 ((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)))
106105anbi1i 627 . . . . . . . . . . . 12 (((𝑥(𝐴 × 𝐴)𝑦𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
10797, 98, 1063bitri 300 . . . . . . . . . . 11 (((𝑥𝑅𝑦𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
108 anass 472 . . . . . . . . . . 11 (((𝑦𝐴 ∧ (𝑥𝐴𝑧𝐴)) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
10996, 107, 1083bitri 300 . . . . . . . . . 10 ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
110109exbii 1855 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
111 vex 3412 . . . . . . . . . . 11 𝑥 ∈ V
112111, 67brco 5739 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧))
113 df-br 5054 . . . . . . . . . 10 (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
114112, 113bitr3i 280 . . . . . . . . 9 (∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
115 df-rex 3067 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))))
116 r19.42v 3263 . . . . . . . . . 10 (∃𝑦𝐴 ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
117115, 116bitr3i 280 . . . . . . . . 9 (∃𝑦(𝑦𝐴 ∧ ((𝑥𝐴𝑧𝐴) ∧ (𝑥𝑅𝑦𝑦𝑅𝑧))) ↔ ((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)))
118110, 114, 1173bitr3ri 305 . . . . . . . 8 (((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) ↔ ⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))))
119 df-br 5054 . . . . . . . 8 (𝑥𝑅𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑅)
120118, 119imbi12i 354 . . . . . . 7 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
1211202albii 1828 . . . . . 6 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
122 r2al 3122 . . . . . . 7 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
123 impexp 454 . . . . . . . 8 ((((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
1241232albii 1828 . . . . . . 7 (∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧((𝑥𝐴𝑧𝐴) → (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
125122, 124bitr4i 281 . . . . . 6 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥𝑧(((𝑥𝐴𝑧𝐴) ∧ ∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
126 relco 6108 . . . . . . 7 Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))
127 ssrel 5654 . . . . . . 7 (Rel ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅)))
128126, 127ax-mp 5 . . . . . 6 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝑧(⟨𝑥, 𝑧⟩ ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → ⟨𝑥, 𝑧⟩ ∈ 𝑅))
129121, 125, 1283bitr4i 306 . . . . 5 (∀𝑥𝐴𝑧𝐴 (∃𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)
13093, 129bitr2i 279 . . . 4 (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
13188, 130anbi12i 630 . . 3 (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
13233, 34, 1313bitr4g 317 . 2 (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)))
13326, 132pm2.61ine 3025 1 (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1541   = wceq 1543  wex 1787  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3408  cin 3865  wss 3866  c0 4237  cop 4547   class class class wbr 5053   I cid 5454   Po wpo 5466   × cxp 5549  cres 5553  ccom 5555  Rel wrel 5556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-id 5455  df-po 5468  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-res 5563
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator