Metamath Proof Explorer

Theorem preddowncl

Description: A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011)

Ref Expression
Assertion preddowncl ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) → ( 𝑋 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
2 predeq3 ⊢ ( 𝑦 = 𝑋 → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )
3 predeq3 ⊢ ( 𝑦 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
4 2 3 eqeq12d ⊢ ( 𝑦 = 𝑋 → ( Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑦 ) ↔ Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
5 1 4 imbi12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ↔ ( 𝑋 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
6 5 imbi2d ⊢ ( 𝑦 = 𝑋 → ( ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) → ( 𝑦 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) → ( 𝑋 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) )
7 predpredss ⊢ ( 𝐵 ⊆ 𝐴 → Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑦 ) )
8 7 ad2antrr ⊢ ( ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑦 ) )
9 predeq3 ⊢ ( 𝑥 = 𝑦 → Pred ( 𝑅 , 𝐴 , 𝑥 ) = Pred ( 𝑅 , 𝐴 , 𝑦 ) )
10 9 sseq1d ⊢ ( 𝑥 = 𝑦 → ( Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ↔ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ) )
11 10 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
12 11 sseld ⊢ ( ( ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → 𝑧 ∈ 𝐵 ) )
13 vex ⊢ 𝑦 ∈ V
14 13 elpredim ⊢ ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → 𝑧 𝑅 𝑦 )
15 12 14 jca2 ⊢ ( ( ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → ( 𝑧 ∈ 𝐵 ∧ 𝑧 𝑅 𝑦 ) ) )
16 vex ⊢ 𝑧 ∈ V
17 16 elpred ⊢ ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐵 , 𝑦 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 𝑅 𝑦 ) ) )
18 17 imbi2d ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → 𝑧 ∈ Pred ( 𝑅 , 𝐵 , 𝑦 ) ) ↔ ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → ( 𝑧 ∈ 𝐵 ∧ 𝑧 𝑅 𝑦 ) ) ) )
19 18 adantl ⊢ ( ( ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → 𝑧 ∈ Pred ( 𝑅 , 𝐵 , 𝑦 ) ) ↔ ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → ( 𝑧 ∈ 𝐵 ∧ 𝑧 𝑅 𝑦 ) ) ) )
20 15 19 mpbird ⊢ ( ( ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) → 𝑧 ∈ Pred ( 𝑅 , 𝐵 , 𝑦 ) ) )
21 20 ssrdv ⊢ ( ( ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐵 , 𝑦 ) )
22 21 adantll ⊢ ( ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐵 , 𝑦 ) )
23 8 22 eqssd ⊢ ( ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑦 ) )
24 23 ex ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) → ( 𝑦 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
25 6 24 vtoclg ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) → ( 𝑋 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
26 25 pm2.43b ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐴 , 𝑥 ) ⊆ 𝐵 ) → ( 𝑋 ∈ 𝐵 → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )