Metamath Proof Explorer

Theorem naddcllem

Description: Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddcllem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +no 𝐵 ) ∈ On ∧ ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑏 ) = ( 𝑐 +no 𝑏 ) )
2 1 eleq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑏 ) ∈ On ↔ ( 𝑐 +no 𝑏 ) ∈ On ) )
3 sneq ⊢ ( 𝑎 = 𝑐 → { 𝑎 } = { 𝑐 } )
4 3 xpeq1d ⊢ ( 𝑎 = 𝑐 → ( { 𝑎 } × 𝑏 ) = ( { 𝑐 } × 𝑏 ) )
5 4 imaeq2d ⊢ ( 𝑎 = 𝑐 → ( +no “ ( { 𝑎 } × 𝑏 ) ) = ( +no “ ( { 𝑐 } × 𝑏 ) ) )
6 5 sseq1d ⊢ ( 𝑎 = 𝑐 → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ) )
7 xpeq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 × { 𝑏 } ) = ( 𝑐 × { 𝑏 } ) )
8 7 imaeq2d ⊢ ( 𝑎 = 𝑐 → ( +no “ ( 𝑎 × { 𝑏 } ) ) = ( +no “ ( 𝑐 × { 𝑏 } ) ) )
9 8 sseq1d ⊢ ( 𝑎 = 𝑐 → ( ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) )
10 6 9 anbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) ) )
11 10 rabbidv ⊢ ( 𝑎 = 𝑐 → { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
12 11 inteqd ⊢ ( 𝑎 = 𝑐 → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
13 1 12 eqeq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ↔ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) )
14 2 13 anbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( 𝑎 +no 𝑏 ) ∈ On ∧ ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ↔ ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ) )
15 oveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝑐 +no 𝑏 ) = ( 𝑐 +no 𝑑 ) )
16 15 eleq1d ⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 +no 𝑏 ) ∈ On ↔ ( 𝑐 +no 𝑑 ) ∈ On ) )
17 xpeq2 ⊢ ( 𝑏 = 𝑑 → ( { 𝑐 } × 𝑏 ) = ( { 𝑐 } × 𝑑 ) )
18 17 imaeq2d ⊢ ( 𝑏 = 𝑑 → ( +no “ ( { 𝑐 } × 𝑏 ) ) = ( +no “ ( { 𝑐 } × 𝑑 ) ) )
19 18 sseq1d ⊢ ( 𝑏 = 𝑑 → ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ) )
20 sneq ⊢ ( 𝑏 = 𝑑 → { 𝑏 } = { 𝑑 } )
21 20 xpeq2d ⊢ ( 𝑏 = 𝑑 → ( 𝑐 × { 𝑏 } ) = ( 𝑐 × { 𝑑 } ) )
22 21 imaeq2d ⊢ ( 𝑏 = 𝑑 → ( +no “ ( 𝑐 × { 𝑏 } ) ) = ( +no “ ( 𝑐 × { 𝑑 } ) ) )
23 22 sseq1d ⊢ ( 𝑏 = 𝑑 → ( ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) )
24 19 23 anbi12d ⊢ ( 𝑏 = 𝑑 → ( ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) ) )
25 24 rabbidv ⊢ ( 𝑏 = 𝑑 → { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } )
26 25 inteqd ⊢ ( 𝑏 = 𝑑 → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } )
27 15 26 eqeq12d ⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ↔ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) )
28 16 27 anbi12d ⊢ ( 𝑏 = 𝑑 → ( ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ↔ ( ( 𝑐 +no 𝑑 ) ∈ On ∧ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ) )
29 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑑 ) = ( 𝑐 +no 𝑑 ) )
30 29 eleq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑑 ) ∈ On ↔ ( 𝑐 +no 𝑑 ) ∈ On ) )
31 3 xpeq1d ⊢ ( 𝑎 = 𝑐 → ( { 𝑎 } × 𝑑 ) = ( { 𝑐 } × 𝑑 ) )
32 31 imaeq2d ⊢ ( 𝑎 = 𝑐 → ( +no “ ( { 𝑎 } × 𝑑 ) ) = ( +no “ ( { 𝑐 } × 𝑑 ) ) )
33 32 sseq1d ⊢ ( 𝑎 = 𝑐 → ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ) )
34 xpeq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 × { 𝑑 } ) = ( 𝑐 × { 𝑑 } ) )
35 34 imaeq2d ⊢ ( 𝑎 = 𝑐 → ( +no “ ( 𝑎 × { 𝑑 } ) ) = ( +no “ ( 𝑐 × { 𝑑 } ) ) )
36 35 sseq1d ⊢ ( 𝑎 = 𝑐 → ( ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) )
37 33 36 anbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) ) )
38 37 rabbidv ⊢ ( 𝑎 = 𝑐 → { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } )
39 38 inteqd ⊢ ( 𝑎 = 𝑐 → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } )
40 29 39 eqeq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ↔ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) )
41 30 40 anbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ↔ ( ( 𝑐 +no 𝑑 ) ∈ On ∧ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ) )
42 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) )
43 42 eleq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no 𝑏 ) ∈ On ↔ ( 𝐴 +no 𝑏 ) ∈ On ) )
44 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
45 44 xpeq1d ⊢ ( 𝑎 = 𝐴 → ( { 𝑎 } × 𝑏 ) = ( { 𝐴 } × 𝑏 ) )
46 45 imaeq2d ⊢ ( 𝑎 = 𝐴 → ( +no “ ( { 𝑎 } × 𝑏 ) ) = ( +no “ ( { 𝐴 } × 𝑏 ) ) )
47 46 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ) )
48 xpeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 × { 𝑏 } ) = ( 𝐴 × { 𝑏 } ) )
49 48 imaeq2d ⊢ ( 𝑎 = 𝐴 → ( +no “ ( 𝑎 × { 𝑏 } ) ) = ( +no “ ( 𝐴 × { 𝑏 } ) ) )
50 49 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) )
51 47 50 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) ) )
52 51 rabbidv ⊢ ( 𝑎 = 𝐴 → { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
53 52 inteqd ⊢ ( 𝑎 = 𝐴 → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
54 42 53 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ↔ ( 𝐴 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) )
55 43 54 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 +no 𝑏 ) ∈ On ∧ ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ↔ ( ( 𝐴 +no 𝑏 ) ∈ On ∧ ( 𝐴 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ) )
56 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) )
57 56 eleq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 +no 𝑏 ) ∈ On ↔ ( 𝐴 +no 𝐵 ) ∈ On ) )
58 xpeq2 ⊢ ( 𝑏 = 𝐵 → ( { 𝐴 } × 𝑏 ) = ( { 𝐴 } × 𝐵 ) )
59 58 imaeq2d ⊢ ( 𝑏 = 𝐵 → ( +no “ ( { 𝐴 } × 𝑏 ) ) = ( +no “ ( { 𝐴 } × 𝐵 ) ) )
60 59 sseq1d ⊢ ( 𝑏 = 𝐵 → ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ) )
61 sneq ⊢ ( 𝑏 = 𝐵 → { 𝑏 } = { 𝐵 } )
62 61 xpeq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐴 × { 𝑏 } ) = ( 𝐴 × { 𝐵 } ) )
63 62 imaeq2d ⊢ ( 𝑏 = 𝐵 → ( +no “ ( 𝐴 × { 𝑏 } ) ) = ( +no “ ( 𝐴 × { 𝐵 } ) ) )
64 63 sseq1d ⊢ ( 𝑏 = 𝐵 → ( ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) )
65 60 64 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) ) )
66 65 rabbidv ⊢ ( 𝑏 = 𝐵 → { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } )
67 66 inteqd ⊢ ( 𝑏 = 𝐵 → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } )
68 56 67 eqeq12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } ↔ ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) )
69 57 68 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 +no 𝑏 ) ∈ On ∧ ( 𝐴 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ↔ ( ( 𝐴 +no 𝐵 ) ∈ On ∧ ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) ) )
70 simpl ⊢ ( ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) → ( 𝑐 +no 𝑏 ) ∈ On )
71 70 ralimi ⊢ ( ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On )
72 71 3ad2ant2 ⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( ( 𝑐 +no 𝑑 ) ∈ On ∧ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On )
73 simpl ⊢ ( ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) → ( 𝑎 +no 𝑑 ) ∈ On )
74 73 ralimi ⊢ ( ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On )
75 74 3ad2ant3 ⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( ( 𝑐 +no 𝑑 ) ∈ On ∧ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On )
76 72 75 jca ⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( ( 𝑐 +no 𝑑 ) ∈ On ∧ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) )
77 df-nadd ⊢ +no = frecs ( { ⟨ 𝑝 , 𝑞 ⟩ ∣ ( 𝑝 ∈ ( On × On ) ∧ 𝑞 ∈ ( On × On ) ∧ ( ( ( 1st ‘ 𝑝 ) E ( 1st ‘ 𝑞 ) ∨ ( 1st ‘ 𝑝 ) = ( 1st ‘ 𝑞 ) ) ∧ ( ( 2nd ‘ 𝑝 ) E ( 2nd ‘ 𝑞 ) ∨ ( 2nd ‘ 𝑝 ) = ( 2nd ‘ 𝑞 ) ) ∧ 𝑝 ≠ 𝑞 ) ) } , ( On × On ) , ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } ) )
78 77 on2recsov ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 +no 𝑏 ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } ) ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) )
79 78 adantr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( 𝑎 +no 𝑏 ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } ) ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) )
80 opex ⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
81 naddfn ⊢ +no Fn ( On × On )
82 fnfun ⊢ ( +no Fn ( On × On ) → Fun +no )
83 81 82 ax-mp ⊢ Fun +no
84 vex ⊢ 𝑎 ∈ V
85 84 sucex ⊢ suc 𝑎 ∈ V
86 vex ⊢ 𝑏 ∈ V
87 86 sucex ⊢ suc 𝑏 ∈ V
88 85 87 xpex ⊢ ( suc 𝑎 × suc 𝑏 ) ∈ V
89 88 difexi ⊢ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∈ V
90 resfunexg ⊢ ( ( Fun +no ∧ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∈ V ) → ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ∈ V )
91 83 89 90 mp2an ⊢ ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ∈ V
92 eloni ⊢ ( 𝑏 ∈ On → Ord 𝑏 )
93 92 ad2antlr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → Ord 𝑏 )
94 ordirr ⊢ ( Ord 𝑏 → ¬ 𝑏 ∈ 𝑏 )
95 93 94 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ¬ 𝑏 ∈ 𝑏 )
96 95 olcd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ¬ 𝑎 ∈ { 𝑎 } ∨ ¬ 𝑏 ∈ 𝑏 ) )
97 ianor ⊢ ( ¬ ( 𝑎 ∈ { 𝑎 } ∧ 𝑏 ∈ 𝑏 ) ↔ ( ¬ 𝑎 ∈ { 𝑎 } ∨ ¬ 𝑏 ∈ 𝑏 ) )
98 opelxp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { 𝑎 } × 𝑏 ) ↔ ( 𝑎 ∈ { 𝑎 } ∧ 𝑏 ∈ 𝑏 ) )
99 97 98 xchnxbir ⊢ ( ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { 𝑎 } × 𝑏 ) ↔ ( ¬ 𝑎 ∈ { 𝑎 } ∨ ¬ 𝑏 ∈ 𝑏 ) )
100 96 99 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { 𝑎 } × 𝑏 ) )
101 84 sucid ⊢ 𝑎 ∈ suc 𝑎
102 snssi ⊢ ( 𝑎 ∈ suc 𝑎 → { 𝑎 } ⊆ suc 𝑎 )
103 101 102 ax-mp ⊢ { 𝑎 } ⊆ suc 𝑎
104 sssucid ⊢ 𝑏 ⊆ suc 𝑏
105 xpss12 ⊢ ( ( { 𝑎 } ⊆ suc 𝑎 ∧ 𝑏 ⊆ suc 𝑏 ) → ( { 𝑎 } × 𝑏 ) ⊆ ( suc 𝑎 × suc 𝑏 ) )
106 103 104 105 mp2an ⊢ ( { 𝑎 } × 𝑏 ) ⊆ ( suc 𝑎 × suc 𝑏 )
107 ssdifsn ⊢ ( ( { 𝑎 } × 𝑏 ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( { 𝑎 } × 𝑏 ) ⊆ ( suc 𝑎 × suc 𝑏 ) ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { 𝑎 } × 𝑏 ) ) )
108 106 107 mpbiran ⊢ ( ( { 𝑎 } × 𝑏 ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { 𝑎 } × 𝑏 ) )
109 100 108 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( { 𝑎 } × 𝑏 ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
110 resima2 ⊢ ( ( { 𝑎 } × 𝑏 ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) = ( +no “ ( { 𝑎 } × 𝑏 ) ) )
111 109 110 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) = ( +no “ ( { 𝑎 } × 𝑏 ) ) )
112 111 sseq1d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ) )
113 eloni ⊢ ( 𝑎 ∈ On → Ord 𝑎 )
114 113 ad2antrr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → Ord 𝑎 )
115 ordirr ⊢ ( Ord 𝑎 → ¬ 𝑎 ∈ 𝑎 )
116 114 115 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ¬ 𝑎 ∈ 𝑎 )
117 116 orcd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ { 𝑏 } ) )
118 ianor ⊢ ( ¬ ( 𝑎 ∈ 𝑎 ∧ 𝑏 ∈ { 𝑏 } ) ↔ ( ¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ { 𝑏 } ) )
119 opelxp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑎 × { 𝑏 } ) ↔ ( 𝑎 ∈ 𝑎 ∧ 𝑏 ∈ { 𝑏 } ) )
120 118 119 xchnxbir ⊢ ( ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑎 × { 𝑏 } ) ↔ ( ¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ { 𝑏 } ) )
121 117 120 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑎 × { 𝑏 } ) )
122 sssucid ⊢ 𝑎 ⊆ suc 𝑎
123 86 sucid ⊢ 𝑏 ∈ suc 𝑏
124 snssi ⊢ ( 𝑏 ∈ suc 𝑏 → { 𝑏 } ⊆ suc 𝑏 )
125 123 124 ax-mp ⊢ { 𝑏 } ⊆ suc 𝑏
126 xpss12 ⊢ ( ( 𝑎 ⊆ suc 𝑎 ∧ { 𝑏 } ⊆ suc 𝑏 ) → ( 𝑎 × { 𝑏 } ) ⊆ ( suc 𝑎 × suc 𝑏 ) )
127 122 125 126 mp2an ⊢ ( 𝑎 × { 𝑏 } ) ⊆ ( suc 𝑎 × suc 𝑏 )
128 ssdifsn ⊢ ( ( 𝑎 × { 𝑏 } ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( ( 𝑎 × { 𝑏 } ) ⊆ ( suc 𝑎 × suc 𝑏 ) ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑎 × { 𝑏 } ) ) )
129 127 128 mpbiran ⊢ ( ( 𝑎 × { 𝑏 } ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑎 × { 𝑏 } ) )
130 121 129 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( 𝑎 × { 𝑏 } ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
131 resima2 ⊢ ( ( 𝑎 × { 𝑏 } ) ⊆ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) → ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) = ( +no “ ( 𝑎 × { 𝑏 } ) ) )
132 130 131 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) = ( +no “ ( 𝑎 × { 𝑏 } ) ) )
133 132 sseq1d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) )
134 112 133 anbi12d ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ) )
135 134 rabbidv ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
136 135 inteqd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∩ { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
137 simprr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On )
138 oveq1 ⊢ ( 𝑡 = 𝑎 → ( 𝑡 +no 𝑑 ) = ( 𝑎 +no 𝑑 ) )
139 138 eleq1d ⊢ ( 𝑡 = 𝑎 → ( ( 𝑡 +no 𝑑 ) ∈ On ↔ ( 𝑎 +no 𝑑 ) ∈ On ) )
140 139 ralbidv ⊢ ( 𝑡 = 𝑎 → ( ∀ 𝑑 ∈ 𝑏 ( 𝑡 +no 𝑑 ) ∈ On ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) )
141 84 140 ralsn ⊢ ( ∀ 𝑡 ∈ { 𝑎 } ∀ 𝑑 ∈ 𝑏 ( 𝑡 +no 𝑑 ) ∈ On ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On )
142 137 141 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∀ 𝑡 ∈ { 𝑎 } ∀ 𝑑 ∈ 𝑏 ( 𝑡 +no 𝑑 ) ∈ On )
143 snssi ⊢ ( 𝑎 ∈ On → { 𝑎 } ⊆ On )
144 onss ⊢ ( 𝑏 ∈ On → 𝑏 ⊆ On )
145 xpss12 ⊢ ( ( { 𝑎 } ⊆ On ∧ 𝑏 ⊆ On ) → ( { 𝑎 } × 𝑏 ) ⊆ ( On × On ) )
146 143 144 145 syl2an ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( { 𝑎 } × 𝑏 ) ⊆ ( On × On ) )
147 146 adantr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( { 𝑎 } × 𝑏 ) ⊆ ( On × On ) )
148 81 fndmi ⊢ dom +no = ( On × On )
149 147 148 sseqtrrdi ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( { 𝑎 } × 𝑏 ) ⊆ dom +no )
150 funimassov ⊢ ( ( Fun +no ∧ ( { 𝑎 } × 𝑏 ) ⊆ dom +no ) → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ On ↔ ∀ 𝑡 ∈ { 𝑎 } ∀ 𝑑 ∈ 𝑏 ( 𝑡 +no 𝑑 ) ∈ On ) )
151 83 149 150 sylancr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ On ↔ ∀ 𝑡 ∈ { 𝑎 } ∀ 𝑑 ∈ 𝑏 ( 𝑡 +no 𝑑 ) ∈ On ) )
152 142 151 mpbird ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ On )
153 simprl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On )
154 oveq2 ⊢ ( 𝑡 = 𝑏 → ( 𝑐 +no 𝑡 ) = ( 𝑐 +no 𝑏 ) )
155 154 eleq1d ⊢ ( 𝑡 = 𝑏 → ( ( 𝑐 +no 𝑡 ) ∈ On ↔ ( 𝑐 +no 𝑏 ) ∈ On ) )
156 86 155 ralsn ⊢ ( ∀ 𝑡 ∈ { 𝑏 } ( 𝑐 +no 𝑡 ) ∈ On ↔ ( 𝑐 +no 𝑏 ) ∈ On )
157 156 ralbii ⊢ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑡 ∈ { 𝑏 } ( 𝑐 +no 𝑡 ) ∈ On ↔ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On )
158 153 157 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∀ 𝑐 ∈ 𝑎 ∀ 𝑡 ∈ { 𝑏 } ( 𝑐 +no 𝑡 ) ∈ On )
159 onss ⊢ ( 𝑎 ∈ On → 𝑎 ⊆ On )
160 snssi ⊢ ( 𝑏 ∈ On → { 𝑏 } ⊆ On )
161 xpss12 ⊢ ( ( 𝑎 ⊆ On ∧ { 𝑏 } ⊆ On ) → ( 𝑎 × { 𝑏 } ) ⊆ ( On × On ) )
162 159 160 161 syl2an ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 × { 𝑏 } ) ⊆ ( On × On ) )
163 162 adantr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( 𝑎 × { 𝑏 } ) ⊆ ( On × On ) )
164 163 148 sseqtrrdi ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( 𝑎 × { 𝑏 } ) ⊆ dom +no )
165 funimassov ⊢ ( ( Fun +no ∧ ( 𝑎 × { 𝑏 } ) ⊆ dom +no ) → ( ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ On ↔ ∀ 𝑐 ∈ 𝑎 ∀ 𝑡 ∈ { 𝑏 } ( 𝑐 +no 𝑡 ) ∈ On ) )
166 83 164 165 sylancr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ On ↔ ∀ 𝑐 ∈ 𝑎 ∀ 𝑡 ∈ { 𝑏 } ( 𝑐 +no 𝑡 ) ∈ On ) )
167 158 166 mpbird ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ On )
168 152 167 unssd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ⊆ On )
169 ssorduni ⊢ ( ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ⊆ On → Ord ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
170 168 169 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → Ord ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
171 snex ⊢ { 𝑎 } ∈ V
172 171 86 xpex ⊢ ( { 𝑎 } × 𝑏 ) ∈ V
173 funimaexg ⊢ ( ( Fun +no ∧ ( { 𝑎 } × 𝑏 ) ∈ V ) → ( +no “ ( { 𝑎 } × 𝑏 ) ) ∈ V )
174 83 172 173 mp2an ⊢ ( +no “ ( { 𝑎 } × 𝑏 ) ) ∈ V
175 snex ⊢ { 𝑏 } ∈ V
176 84 175 xpex ⊢ ( 𝑎 × { 𝑏 } ) ∈ V
177 funimaexg ⊢ ( ( Fun +no ∧ ( 𝑎 × { 𝑏 } ) ∈ V ) → ( +no “ ( 𝑎 × { 𝑏 } ) ) ∈ V )
178 83 176 177 mp2an ⊢ ( +no “ ( 𝑎 × { 𝑏 } ) ) ∈ V
179 174 178 unex ⊢ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ V
180 179 uniex ⊢ ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ V
181 180 elon ⊢ ( ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ On ↔ Ord ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
182 170 181 sylibr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ On )
183 sucelon ⊢ ( ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ On ↔ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ On )
184 182 183 sylib ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ On )
185 onsucuni ⊢ ( ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ⊆ On → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
186 168 185 syl ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
187 186 unssad ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
188 186 unssbd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) )
189 sseq2 ⊢ ( 𝑥 = suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) → ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ) )
190 sseq2 ⊢ ( 𝑥 = suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) → ( ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ) )
191 189 190 anbi12d ⊢ ( 𝑥 = suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) → ( ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ) ) )
192 191 rspcev ⊢ ( ( suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∈ On ∧ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ suc ∪ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ∪ ( +no “ ( 𝑎 × { 𝑏 } ) ) ) ) ) → ∃ 𝑥 ∈ On ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) )
193 184 187 188 192 syl12anc ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∃ 𝑥 ∈ On ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) )
194 onintrab2 ⊢ ( ∃ 𝑥 ∈ On ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ∈ On )
195 193 194 sylib ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ∈ On )
196 136 195 eqeltrd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ∩ { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ∈ On )
197 84 86 op1std ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1st ‘ 𝑡 ) = 𝑎 )
198 197 sneqd ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → { ( 1st ‘ 𝑡 ) } = { 𝑎 } )
199 84 86 op2ndd ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑡 ) = 𝑏 )
200 198 199 xpeq12d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) = ( { 𝑎 } × 𝑏 ) )
201 200 imaeq2d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) = ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) )
202 201 sseq1d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ↔ ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ) )
203 199 sneqd ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → { ( 2nd ‘ 𝑡 ) } = { 𝑏 } )
204 197 203 xpeq12d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) = ( 𝑎 × { 𝑏 } ) )
205 204 imaeq2d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) = ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) )
206 205 sseq1d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ↔ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) )
207 202 206 anbi12d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) ↔ ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ) )
208 207 rabbidv ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
209 208 inteqd ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
210 imaeq1 ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) = ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) )
211 210 sseq1d ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ↔ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ) )
212 imaeq1 ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) = ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) )
213 212 sseq1d ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → ( ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ↔ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) )
214 211 213 anbi12d ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → ( ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ↔ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) ) )
215 214 rabbidv ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
216 215 inteqd ⊢ ( 𝑓 = ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) → ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
217 eqid ⊢ ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } ) = ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } )
218 209 216 217 ovmpog ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ V ∧ ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ∈ V ∧ ∩ { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ∈ On ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } ) ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) = ∩ { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
219 80 91 196 218 mp3an12i ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( 𝑡 ∈ V , 𝑓 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ ( ( 𝑓 “ ( { ( 1st ‘ 𝑡 ) } × ( 2nd ‘ 𝑡 ) ) ) ⊆ 𝑥 ∧ ( 𝑓 “ ( ( 1st ‘ 𝑡 ) × { ( 2nd ‘ 𝑡 ) } ) ) ⊆ 𝑥 ) } ) ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) ) = ∩ { 𝑥 ∈ On ∣ ( ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( ( +no ↾ ( ( suc 𝑎 × suc 𝑏 ) ∖ { ⟨ 𝑎 , 𝑏 ⟩ } ) ) “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
220 79 219 136 3eqtrd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } )
221 220 195 eqeltrd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( 𝑎 +no 𝑏 ) ∈ On )
222 221 220 jca ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) ) → ( ( 𝑎 +no 𝑏 ) ∈ On ∧ ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) )
223 222 ex ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ On ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ On ) → ( ( 𝑎 +no 𝑏 ) ∈ On ∧ ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ) )
224 76 223 syl5 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( ( 𝑐 +no 𝑑 ) ∈ On ∧ ( 𝑐 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ On ∧ ( 𝑐 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑐 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑐 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ∧ ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ On ∧ ( 𝑎 +no 𝑑 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑑 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑑 } ) ) ⊆ 𝑥 ) } ) ) → ( ( 𝑎 +no 𝑏 ) ∈ On ∧ ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝑎 } × 𝑏 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝑎 × { 𝑏 } ) ) ⊆ 𝑥 ) } ) ) )
225 14 28 41 55 69 224 on2ind ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +no 𝐵 ) ∈ On ∧ ( 𝐴 +no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ( ( +no “ ( { 𝐴 } × 𝐵 ) ) ⊆ 𝑥 ∧ ( +no “ ( 𝐴 × { 𝐵 } ) ) ⊆ 𝑥 ) } ) )