Metamath Proof Explorer

Theorem predpo

Description: Property of the precessor class for partial orderings. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion predpo ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 predel ⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 ∈ 𝐴 )
2 elpredg ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )
3 2 adantll ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )
4 potr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) )
5 4 3exp2 ⊢ ( 𝑅 Po 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑌 ∈ 𝐴 → ( 𝑋 ∈ 𝐴 → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) ) ) )
6 5 com24 ⊢ ( 𝑅 Po 𝐴 → ( 𝑋 ∈ 𝐴 → ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) ) ) )
7 6 imp31 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) )
8 7 com13 ⊢ ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → ( 𝑧 ∈ 𝐴 → ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑧 𝑅 𝑋 ) ) )
9 8 ex ⊢ ( 𝑧 𝑅 𝑌 → ( 𝑌 𝑅 𝑋 → ( 𝑧 ∈ 𝐴 → ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑧 𝑅 𝑋 ) ) ) )
10 9 com14 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 𝑅 𝑋 → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) )
11 3 10 sylbid ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) )
12 11 ex ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ 𝐴 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) ) )
13 12 com23 ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) ) )
14 13 3imp ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) )
15 14 imdistand ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) → ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
16 vex ⊢ 𝑧 ∈ V
17 16 elpred ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) ) )
18 17 3ad2ant3 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) ) )
19 16 elpred ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
20 19 adantl ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
21 20 3ad2ant1 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) )
22 15 18 21 3imtr4d ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) → 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
23 22 ssrdv ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
24 23 3exp ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑌 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
25 1 24 mpdi ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )