| Step | Hyp | Ref | Expression | 
						
							| 1 |  | simp3 | ⊢ ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  →  𝐶  ∈  On ) | 
						
							| 2 |  | 0elon | ⊢ ∅  ∈  On | 
						
							| 3 |  | ordelon | ⊢ ( ( Ord  𝐴  ∧  𝑥  ∈  𝐴 )  →  𝑥  ∈  On ) | 
						
							| 4 | 3 | 3ad2antl1 | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  𝑥  ∈  On ) | 
						
							| 5 |  | naddcom | ⊢ ( ( ∅  ∈  On  ∧  𝑥  ∈  On )  →  ( ∅  +no  𝑥 )  =  ( 𝑥  +no  ∅ ) ) | 
						
							| 6 | 2 4 5 | sylancr | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( ∅  +no  𝑥 )  =  ( 𝑥  +no  ∅ ) ) | 
						
							| 7 |  | naddrid | ⊢ ( 𝑥  ∈  On  →  ( 𝑥  +no  ∅ )  =  𝑥 ) | 
						
							| 8 | 4 7 | syl | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( 𝑥  +no  ∅ )  =  𝑥 ) | 
						
							| 9 | 6 8 | eqtrd | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( ∅  +no  𝑥 )  =  𝑥 ) | 
						
							| 10 |  | 0ss | ⊢ ∅  ⊆  𝐵 | 
						
							| 11 |  | simpl2 | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  𝐵  ∈  On ) | 
						
							| 12 |  | naddssim | ⊢ ( ( ∅  ∈  On  ∧  𝐵  ∈  On  ∧  𝑥  ∈  On )  →  ( ∅  ⊆  𝐵  →  ( ∅  +no  𝑥 )  ⊆  ( 𝐵  +no  𝑥 ) ) ) | 
						
							| 13 | 2 11 4 12 | mp3an2i | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( ∅  ⊆  𝐵  →  ( ∅  +no  𝑥 )  ⊆  ( 𝐵  +no  𝑥 ) ) ) | 
						
							| 14 | 10 13 | mpi | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( ∅  +no  𝑥 )  ⊆  ( 𝐵  +no  𝑥 ) ) | 
						
							| 15 | 9 14 | eqsstrrd | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  𝑥  ⊆  ( 𝐵  +no  𝑥 ) ) | 
						
							| 16 |  | simpl3 | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  𝐶  ∈  On ) | 
						
							| 17 |  | ontr2 | ⊢ ( ( 𝑥  ∈  On  ∧  𝐶  ∈  On )  →  ( ( 𝑥  ⊆  ( 𝐵  +no  𝑥 )  ∧  ( 𝐵  +no  𝑥 )  ∈  𝐶 )  →  𝑥  ∈  𝐶 ) ) | 
						
							| 18 | 4 16 17 | syl2anc | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( ( 𝑥  ⊆  ( 𝐵  +no  𝑥 )  ∧  ( 𝐵  +no  𝑥 )  ∈  𝐶 )  →  𝑥  ∈  𝐶 ) ) | 
						
							| 19 | 15 18 | mpand | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴 )  →  ( ( 𝐵  +no  𝑥 )  ∈  𝐶  →  𝑥  ∈  𝐶 ) ) | 
						
							| 20 | 19 | 3impia | ⊢ ( ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  ∧  𝑥  ∈  𝐴  ∧  ( 𝐵  +no  𝑥 )  ∈  𝐶 )  →  𝑥  ∈  𝐶 ) | 
						
							| 21 | 20 | rabssdv | ⊢ ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  →  { 𝑥  ∈  𝐴  ∣  ( 𝐵  +no  𝑥 )  ∈  𝐶 }  ⊆  𝐶 ) | 
						
							| 22 | 1 21 | ssexd | ⊢ ( ( Ord  𝐴  ∧  𝐵  ∈  On  ∧  𝐶  ∈  On )  →  { 𝑥  ∈  𝐴  ∣  ( 𝐵  +no  𝑥 )  ∈  𝐶 }  ∈  V ) |