Metamath Proof Explorer

Theorem lrrecpred

Description: Finally, we calculate the value of the predecessor class over R . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
Assertion lrrecpred ⊢ A ∈ No → Pred R No A = L ⁡ A ∪ R ⁡ A

Proof

Step Hyp Ref Expression
1 lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
2 dfpred3g ⊢ A ∈ No → Pred R No A = b ∈ No | b R A
3 1 lrrecval ⊢ b ∈ No ∧ A ∈ No → b R A ↔ b ∈ L ⁡ A ∪ R ⁡ A
4 3 ancoms ⊢ A ∈ No ∧ b ∈ No → b R A ↔ b ∈ L ⁡ A ∪ R ⁡ A
5 4 rabbidva ⊢ A ∈ No → b ∈ No | b R A = b ∈ No | b ∈ L ⁡ A ∪ R ⁡ A
6 dfrab2 ⊢ b ∈ No | b ∈ L ⁡ A ∪ R ⁡ A = b | b ∈ L ⁡ A ∪ R ⁡ A ∩ No
7 abid2 ⊢ b | b ∈ L ⁡ A ∪ R ⁡ A = L ⁡ A ∪ R ⁡ A
8 7 ineq1i ⊢ b | b ∈ L ⁡ A ∪ R ⁡ A ∩ No = L ⁡ A ∪ R ⁡ A ∩ No
9 6 8 eqtri ⊢ b ∈ No | b ∈ L ⁡ A ∪ R ⁡ A = L ⁡ A ∪ R ⁡ A ∩ No
10 5 9 eqtrdi ⊢ A ∈ No → b ∈ No | b R A = L ⁡ A ∪ R ⁡ A ∩ No
11 leftssno ⊢ L ⁡ A ⊆ No
12 11 a1i ⊢ A ∈ No → L ⁡ A ⊆ No
13 rightssno ⊢ R ⁡ A ⊆ No
14 13 a1i ⊢ A ∈ No → R ⁡ A ⊆ No
15 12 14 unssd ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A ⊆ No
16 df-ss ⊢ L ⁡ A ∪ R ⁡ A ⊆ No ↔ L ⁡ A ∪ R ⁡ A ∩ No = L ⁡ A ∪ R ⁡ A
17 15 16 sylib ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A ∩ No = L ⁡ A ∪ R ⁡ A
18 2 10 17 3eqtrd ⊢ A ∈ No → Pred R No A = L ⁡ A ∪ R ⁡ A