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 28 31 naddcld ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐴 +no 𝑤 ) ∈ On )
33 simplrl ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → 𝑥 ∈ On )
34 ontr2 ⊢ ( ( ( 𝐴 +no 𝑤 ) ∈ On ∧ 𝑥 ∈ On ) → ( ( ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) ∧ ( 𝐵 +no 𝑤 ) ∈ 𝑥 ) → ( 𝐴 +no 𝑤 ) ∈ 𝑥 ) )
35 32 33 34 syl2anc ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( ( ( 𝐴 +no 𝑤 ) ⊆ ( 𝐵 +no 𝑤 ) ∧ ( 𝐵 +no 𝑤 ) ∈ 𝑥 ) → ( 𝐴 +no 𝑤 ) ∈ 𝑥 ) )
36 19 24 35 mp2and ⊢ ( ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑐 ) → ( 𝐴 +no 𝑤 ) ∈ 𝑥 )
37 36 ralrimiva ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 )
38 simpllr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → 𝐴 ⊆ 𝐵 )
39 simprrr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 )
40 ssralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 → ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) )
41 38 39 40 sylc ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 )
42 37 41 jca ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ ( 𝑥 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) ) → ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) )
43 42 expr ⊢ ( ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) → ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) ) )
44 43 ss2rabdv ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
45 intss ⊢ ( { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
46 44 45 syl ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } ⊆ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
47 simplll ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → 𝑐 ∈ On )
48 naddov2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑐 ∈ On ) → ( 𝐴 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
49 26 47 48 syl2anc ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑤 ∈ 𝑐 ( 𝐴 +no 𝑤 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
50 simplrr ⊢ ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ On )
51 50 adantr ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → 𝐵 ∈ On )
52 naddov2 ⊢ ( ( 𝐵 ∈ On ∧ 𝑐 ∈ On ) → ( 𝐵 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
53 51 47 52 syl2anc ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐵 +no 𝑐 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑦 ∈ 𝑐 ( 𝐵 +no 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 +no 𝑐 ) ∈ 𝑥 ) } )
54 46 49 53 3sstr4d ⊢ ( ( ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) )
55 54 exp31 ⊢ ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) )
56 55 a2d ⊢ ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) )
57 56 ex ⊢ ( 𝑐 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ) )
58 57 a2d ⊢ ( 𝑐 ∈ On → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∀ 𝑑 ∈ 𝑐 ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ) )
59 14 58 biimtrid ⊢ ( 𝑐 ∈ On → ( ∀ 𝑑 ∈ 𝑐 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑑 ) ⊆ ( 𝐵 +no 𝑑 ) ) ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝑐 ) ⊆ ( 𝐵 +no 𝑐 ) ) ) ) )
60 5 10 59 tfis3 ⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) ) )
61 60 com12 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ On → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) ) )
62 61 3impia ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) )