Metamath Proof Explorer

Theorem naddssim

Description: Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024)

Ref Expression
Assertion naddssim ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑐 = 𝑑 → ( 𝐴 +no 𝑐 ) = ( 𝐴 +no 𝑑 ) )
2 oveq2 ⊢ ( 𝑐 = 𝑑 → ( 𝐵 +no 𝑐 ) = ( 𝐵 +no 𝑑 ) )
3 1 2 sseq12d ⊢ ( 𝑐 = 𝑑 → ( ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ↔ ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) )
4 3 imbi2d ⊢ ( 𝑐 = 𝑑 → ( ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ↔ ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) )
5 4 imbi2d ⊢ ( 𝑐 = 𝑑 → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ↔ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) ) )
6 oveq2 ⊢ ( 𝑐 = 𝐶 → ( 𝐴 +no 𝑐 ) = ( 𝐴 +no 𝐶 ) )
7 oveq2 ⊢ ( 𝑐 = 𝐶 → ( 𝐵 +no 𝑐 ) = ( 𝐵 +no 𝐶 ) )
8 6 7 sseq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ↔ ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) )
9 8 imbi2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ↔ ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) ) )
10 9 imbi2d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ↔ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) ) ) )
11 r19.21v ⊢ ( ∀ 𝑑 ∈ 𝑐 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) ↔ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∀ 𝑑 ∈ 𝑐 ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) )
12 r19.21v ⊢ ( ∀ 𝑑 ∈ 𝑐 ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ↔ ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) )
13 12 imbi2i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∀ 𝑑 ∈ 𝑐 ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) ↔ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) )
14 11 13 bitri ⊢ ( ∀ 𝑑 ∈ 𝑐 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) ↔ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) )
15 oveq2 ⊢ ( 𝑑 = 𝑤 → ( 𝐴 +no 𝑑 ) = ( 𝐴 +no 𝑤 ) )
16 oveq2 ⊢ ( 𝑑 = 𝑤 → ( 𝐵 +no 𝑑 ) = ( 𝐵 +no 𝑤 ) )
17 15 16 sseq12d ⊢ ( 𝑑 = 𝑤 → ( ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ↔ ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) ) )
18 17 rspccva ⊢ ( ( ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) )
19 18 ad4ant24 ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) )
20 simprrl ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 )
21 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐵 +no 𝑦 ) = ( 𝐵 +no 𝑤 ) )
22 21 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐵 +no 𝑦 ) ∈ 𝑥 ↔ ( 𝐵 +no 𝑤 ) ∈ 𝑥 ) )
23 22 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ 𝑤 ∈ 𝑐 ) → ( 𝐵 +no 𝑤 ) ∈ 𝑥 )
24 20 23 sylan ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐵 +no 𝑤 ) ∈ 𝑥 )
25 simplrl ⊢ ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ On )
26 25 adantr ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → 𝐴 ∈ On )
27 26 adantr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → 𝐴 ∈ On )
28 27 adantr ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → 𝐴 ∈ On )
29 simp-4l ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → 𝑐 ∈ On )
30 onelon ⊢ ( ( 𝑐 ∈ On ∧ 𝑤 ∈ 𝑐 ) → 𝑤 ∈ On )
31 29 30 sylan ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → 𝑤 ∈ On )
32 naddcl ⊢ ( ( 𝐴 ∈ On ∧ 𝑤 ∈ On ) → ( 𝐴 +no 𝑤 ) ∈ On )
33 28 31 32 syl2anc ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐴 +no 𝑤 ) ∈ On )
34 simplrl ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → 𝑥 ∈ On )
35 ontr2 ⊢ ( ( ( 𝐴 +no 𝑤 ) ∈ On ∧ 𝑥 ∈ On ) → ( ( ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) ∧ ( 𝐵 +no 𝑤 ) ∈ 𝑥 ) → ( 𝐴 +no 𝑤 ) ∈ 𝑥 ) )
36 33 34 35 syl2anc ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( ( ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) ∧ ( 𝐵 +no 𝑤 ) ∈ 𝑥 ) → ( 𝐴 +no 𝑤 ) ∈ 𝑥 ) )
37 19 24 36 mp2and ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐴 +no 𝑤 ) ∈ 𝑥 )
38 37 ralrimiva ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 )
39 simpllr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → 𝐴 ⊆ 𝐵 )
40 simprrr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 )
41 ssralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 → ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) )
42 39 40 41 sylc ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 )
43 38 42 jca ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) )
44 43 expr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) → ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) )
45 44 ss2rabdv ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
46 intss ⊢ ( { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
47 45 46 syl ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
48 simplll ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → 𝑐 ∈ On )
49 naddov2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑐 ∈ On ) → ( 𝐴 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
50 26 48 49 syl2anc ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
51 simplrr ⊢ ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ On )
52 51 adantr ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → 𝐵 ∈ On )
53 naddov2 ⊢ ( ( 𝐵 ∈ On ∧ 𝑐 ∈ On ) → ( 𝐵 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
54 52 48 53 syl2anc ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐵 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
55 47 50 54 3sstr4d ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) )
56 55 exp31 ⊢ ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) )
57 56 a2d ⊢ ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) )
58 57 ex ⊢ ( 𝑐 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ) )
59 58 a2d ⊢ ( 𝑐 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ) )
60 14 59 biimtrid ⊢ ( 𝑐 ∈ On → ( ∀ 𝑑 ∈ 𝑐 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ) )
61 5 10 60 tfis3 ⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) ) )
62 61 com12 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ On → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) ) )
63 62 3impia ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) )