Metamath Proof Explorer

Theorem noxpordpred

Description: Next we calculate the predecessor class of the relationship. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses noxpord.1 ⊢ R = a b | a ∈ L ⁡ b ∪ R ⁡ b
noxpord.2 ⊢ S = x y | x ∈ No × No ∧ y ∈ No × No ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x R 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
Assertion noxpordpred ⊢ A ∈ No ∧ B ∈ No → Pred S No × No A B = L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B

Proof

Step Hyp Ref Expression
1 noxpord.1 ⊢ R = a b | a ∈ L ⁡ b ∪ R ⁡ b
2 noxpord.2 ⊢ S = x y | x ∈ No × No ∧ y ∈ No × No ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x R 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
3 2 xpord2pred ⊢ A ∈ No ∧ B ∈ No → Pred S No × No A B = Pred R No A ∪ A × Pred R No B ∪ B ∖ A B
4 1 lrrecpred ⊢ A ∈ No → Pred R No A = L ⁡ A ∪ R ⁡ A
5 4 adantr ⊢ A ∈ No ∧ B ∈ No → Pred R No A = L ⁡ A ∪ R ⁡ A
6 5 uneq1d ⊢ A ∈ No ∧ B ∈ No → Pred R No A ∪ A = L ⁡ A ∪ R ⁡ A ∪ A
7 1 lrrecpred ⊢ B ∈ No → Pred R No B = L ⁡ B ∪ R ⁡ B
8 7 adantl ⊢ A ∈ No ∧ B ∈ No → Pred R No B = L ⁡ B ∪ R ⁡ B
9 8 uneq1d ⊢ A ∈ No ∧ B ∈ No → Pred R No B ∪ B = L ⁡ B ∪ R ⁡ B ∪ B
10 6 9 xpeq12d ⊢ A ∈ No ∧ B ∈ No → Pred R No A ∪ A × Pred R No B ∪ B = L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B
11 10 difeq1d ⊢ A ∈ No ∧ B ∈ No → Pred R No A ∪ A × Pred R No B ∪ B ∖ A B = L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B
12 3 11 eqtrd ⊢ A ∈ No ∧ B ∈ No → Pred S No × No A B = L ⁡ A ∪ R ⁡ A ∪ A × L ⁡ B ∪ R ⁡ B ∪ B ∖ A B