Metamath Proof Explorer

Theorem predtrss

Description: If R is transitive over A and Y R X , then Pred ( R , A , Y ) is a subclass of Pred ( R , A , X ) . (Contributed by Scott Fenton, 28-Oct-2024)

Ref Expression
Assertion predtrss ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
2 predel ⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 ∈ 𝐴 )
3 2 3ad2ant2 ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 )
4 3 adantr ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 )
5 brxp ⊢ ( 𝑧 ( 𝐴 × 𝐴 ) 𝑌 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) )
6 1 4 5 sylanbrc ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ( 𝐴 × 𝐴 ) 𝑌 )
7 brin ⊢ ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ↔ ( 𝑧 𝑅 𝑌 ∧ 𝑧 ( 𝐴 × 𝐴 ) 𝑌 ) )
8 predbrg ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 𝑅 𝑋 )
9 8 ancoms ⊢ ( ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑌 𝑅 𝑋 )
10 9 3adant1 ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑌 𝑅 𝑋 )
11 10 adantr ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑌 𝑅 𝑋 )
12 simpl3 ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
13 brxp ⊢ ( 𝑌 ( 𝐴 × 𝐴 ) 𝑋 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
14 4 12 13 sylanbrc ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑌 ( 𝐴 × 𝐴 ) 𝑋 )
15 brin ⊢ ( 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ↔ ( 𝑌 𝑅 𝑋 ∧ 𝑌 ( 𝐴 × 𝐴 ) 𝑋 ) )
16 11 14 15 sylanbrc ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 )
17 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ↔ 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ) )
18 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ↔ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) )
19 17 18 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ↔ ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ∧ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ) )
20 19 spcegv ⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ∧ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) → ∃ 𝑦 ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ) )
21 20 3ad2ant2 ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ∧ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) → ∃ 𝑦 ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ) )
22 21 adantr ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ∧ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) → ∃ 𝑦 ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ) )
23 vex ⊢ 𝑧 ∈ V
24 brcog ⊢ ( ( 𝑧 ∈ V ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) 𝑋 ↔ ∃ 𝑦 ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ) )
25 23 12 24 sylancr ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) 𝑋 ↔ ∃ 𝑦 ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) ) )
26 22 25 sylibrd ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ∧ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) → 𝑧 ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) 𝑋 ) )
27 simpl1 ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 )
28 27 ssbrd ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) 𝑋 → 𝑧 𝑅 𝑋 ) )
29 26 28 syld ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 ∧ 𝑌 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑋 ) → 𝑧 𝑅 𝑋 ) )
30 16 29 mpan2d ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑌 → 𝑧 𝑅 𝑋 ) )
31 7 30 syl5bir ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 𝑅 𝑌 ∧ 𝑧 ( 𝐴 × 𝐴 ) 𝑌 ) → 𝑧 𝑅 𝑋 ) )
32 6 31 mpan2d ⊢ ( ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) )
33 32 imdistanda ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) → ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
34 23 elpred ⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) ) )
35 34 3ad2ant2 ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) ) )
36 23 elpred ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
37 36 3ad2ant3 ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
38 33 35 37 3imtr4d ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) → 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
39 38 ssrdv ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )