Metamath Proof Explorer

Theorem nadd2rabtr

Description: The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024)

Ref Expression
Assertion nadd2rabtr ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → Tr { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } )

Proof

Step Hyp Ref Expression
1 simpll1 ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → Ord 𝐴 )
2 simplr ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → 𝑦 ∈ 𝐴 )
3 ordelss ⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ 𝐴 )
4 1 2 3 syl2anc ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → 𝑦 ⊆ 𝐴 )
5 simpll3 ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → 𝐶 ∈ On )
6 5 adantr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → 𝐶 ∈ On )
7 simpr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑦 )
8 1 adantr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → Ord 𝐴 )
9 simpllr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ 𝐴 )
10 ordelon ⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
11 8 9 10 syl2anc ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ On )
12 onelon ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On )
13 11 7 12 syl2anc ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On )
14 simpll2 ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → 𝐵 ∈ On )
15 14 adantr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ On )
16 naddel2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝐵 +no 𝑥 ) ∈ ( 𝐵 +no 𝑦 ) ) )
17 13 11 15 16 syl3anc ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝐵 +no 𝑥 ) ∈ ( 𝐵 +no 𝑦 ) ) )
18 7 17 mpbid ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝐵 +no 𝑥 ) ∈ ( 𝐵 +no 𝑦 ) )
19 simplr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝐵 +no 𝑦 ) ∈ 𝐶 )
20 18 19 jca ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐵 +no 𝑥 ) ∈ ( 𝐵 +no 𝑦 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) )
21 ontr1 ⊢ ( 𝐶 ∈ On → ( ( ( 𝐵 +no 𝑥 ) ∈ ( 𝐵 +no 𝑦 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → ( 𝐵 +no 𝑥 ) ∈ 𝐶 ) )
22 6 20 21 sylc ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝐵 +no 𝑥 ) ∈ 𝐶 )
23 4 22 ssrabdv ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) → 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } )
24 23 ex ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐵 +no 𝑦 ) ∈ 𝐶 → 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ) )
25 24 ralrimiva ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ∀ 𝑦 ∈ 𝐴 ( ( 𝐵 +no 𝑦 ) ∈ 𝐶 → 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ) )
26 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 +no 𝑥 ) = ( 𝐵 +no 𝑦 ) )
27 26 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 +no 𝑥 ) ∈ 𝐶 ↔ ( 𝐵 +no 𝑦 ) ∈ 𝐶 ) )
28 27 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝐵 +no 𝑦 ) ∈ 𝐶 → 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ) )
29 25 28 sylibr ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } )
30 dftr3 ⊢ ( Tr { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } 𝑦 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } )
31 29 30 sylibr ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → Tr { 𝑥 ∈ 𝐴 ∣ ( 𝐵 +no 𝑥 ) ∈ 𝐶 } )