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 syl5bi ( 𝑐 ∈ 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 𝐶 ) ) )