MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  naddcllem Structured version   Visualization version   GIF version

Theorem naddcllem 8623
Description: Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024.)
Assertion
Ref Expression
naddcllem ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem naddcllem
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑓 𝑡 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7365 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
21eleq1d 2823 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3 sneq 4597 . . . . . . . . . 10 (𝑎 = 𝑐 → {𝑎} = {𝑐})
43xpeq1d 5663 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
54imaeq2d 6014 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
65sseq1d 3976 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7 xpeq1 5648 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
87imaeq2d 6014 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
98sseq1d 3976 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
106, 9anbi12d 632 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
1110rabbidv 3416 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
1211inteqd 4913 . . . 4 (𝑎 = 𝑐 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
131, 12eqeq12d 2753 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}))
142, 13anbi12d 632 . 2 (𝑎 = 𝑐 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})))
15 oveq2 7366 . . . 4 (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
1615eleq1d 2823 . . 3 (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17 xpeq2 5655 . . . . . . . . 9 (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
1817imaeq2d 6014 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
1918sseq1d 3976 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20 sneq 4597 . . . . . . . . . 10 (𝑏 = 𝑑 → {𝑏} = {𝑑})
2120xpeq2d 5664 . . . . . . . . 9 (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
2221imaeq2d 6014 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
2322sseq1d 3976 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
2419, 23anbi12d 632 . . . . . 6 (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
2524rabbidv 3416 . . . . 5 (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2625inteqd 4913 . . . 4 (𝑏 = 𝑑 {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2715, 26eqeq12d 2753 . . 3 (𝑏 = 𝑑 → ((𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
2816, 27anbi12d 632 . 2 (𝑏 = 𝑑 → (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
29 oveq1 7365 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
3029eleq1d 2823 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
313xpeq1d 5663 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
3231imaeq2d 6014 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
3332sseq1d 3976 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34 xpeq1 5648 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
3534imaeq2d 6014 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
3635sseq1d 3976 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
3733, 36anbi12d 632 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
3837rabbidv 3416 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
3938inteqd 4913 . . . 4 (𝑎 = 𝑐 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
4029, 39eqeq12d 2753 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
4130, 40anbi12d 632 . 2 (𝑎 = 𝑐 → (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
42 oveq1 7365 . . . 4 (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
4342eleq1d 2823 . . 3 (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44 sneq 4597 . . . . . . . . . 10 (𝑎 = 𝐴 → {𝑎} = {𝐴})
4544xpeq1d 5663 . . . . . . . . 9 (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
4645imaeq2d 6014 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
4746sseq1d 3976 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48 xpeq1 5648 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
4948imaeq2d 6014 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
5049sseq1d 3976 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
5147, 50anbi12d 632 . . . . . 6 (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
5251rabbidv 3416 . . . . 5 (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5352inteqd 4913 . . . 4 (𝑎 = 𝐴 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5442, 53eqeq12d 2753 . . 3 (𝑎 = 𝐴 → ((𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}))
5543, 54anbi12d 632 . 2 (𝑎 = 𝐴 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})))
56 oveq2 7366 . . . 4 (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
5756eleq1d 2823 . . 3 (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58 xpeq2 5655 . . . . . . . . 9 (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
5958imaeq2d 6014 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
6059sseq1d 3976 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61 sneq 4597 . . . . . . . . . 10 (𝑏 = 𝐵 → {𝑏} = {𝐵})
6261xpeq2d 5664 . . . . . . . . 9 (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
6362imaeq2d 6014 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
6463sseq1d 3976 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
6560, 64anbi12d 632 . . . . . 6 (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
6665rabbidv 3416 . . . . 5 (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6766inteqd 4913 . . . 4 (𝑏 = 𝐵 {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6856, 67eqeq12d 2753 . . 3 (𝑏 = 𝐵 → ((𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
6957, 68anbi12d 632 . 2 (𝑏 = 𝐵 → (((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})))
70 simpl 484 . . . . . 6 (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
7170ralimi 3087 . . . . 5 (∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
72713ad2ant2 1135 . . . 4 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
73 simpl 484 . . . . . 6 (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
7473ralimi 3087 . . . . 5 (∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
75743ad2ant3 1136 . . . 4 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
7672, 75jca 513 . . 3 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +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 8613 . . . . . . . . 9 +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𝑡)})) ⊆ 𝑥)}))
7877on2recsov 8615 . . . . . . . 8 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
7978adantr 482 . . . . . . 7 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
80 opex 5422 . . . . . . . 8 𝑎, 𝑏⟩ ∈ V
81 naddfn 8622 . . . . . . . . . 10 +no Fn (On × On)
82 fnfun 6603 . . . . . . . . . 10 ( +no Fn (On × On) → Fun +no )
8381, 82ax-mp 5 . . . . . . . . 9 Fun +no
84 vex 3450 . . . . . . . . . . . 12 𝑎 ∈ V
8584sucex 7742 . . . . . . . . . . 11 suc 𝑎 ∈ V
86 vex 3450 . . . . . . . . . . . 12 𝑏 ∈ V
8786sucex 7742 . . . . . . . . . . 11 suc 𝑏 ∈ V
8885, 87xpex 7688 . . . . . . . . . 10 (suc 𝑎 × suc 𝑏) ∈ V
8988difexi 5286 . . . . . . . . 9 ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90 resfunexg 7166 . . . . . . . . 9 ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
9183, 89, 90mp2an 691 . . . . . . . 8 ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92 eloni 6328 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ On → Ord 𝑏)
9392ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94 ordirr 6336 . . . . . . . . . . . . . . . . . 18 (Ord 𝑏 → ¬ 𝑏𝑏)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏𝑏)
9695olcd 873 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
97 ianor 981 . . . . . . . . . . . . . . . . 17 (¬ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
98 opelxp 5670 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏))
9997, 98xchnxbir 333 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
10096, 99sylibr 233 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
10184sucid 6400 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ suc 𝑎
102 snssi 4769 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑎} ⊆ suc 𝑎
104 sssucid 6398 . . . . . . . . . . . . . . . . 17 𝑏 ⊆ suc 𝑏
105 xpss12 5649 . . . . . . . . . . . . . . . . 17 (({𝑎} ⊆ suc 𝑎𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106103, 104, 105mp2an 691 . . . . . . . . . . . . . . . 16 ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107 ssdifsn 4749 . . . . . . . . . . . . . . . 16 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108106, 107mpbiran 708 . . . . . . . . . . . . . . 15 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109100, 108sylibr 233 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110 resima2 5973 . . . . . . . . . . . . . 14 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
111109, 110syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
112111sseq1d 3976 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113 eloni 6328 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ On → Ord 𝑎)
114113ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115 ordirr 6336 . . . . . . . . . . . . . . . . . 18 (Ord 𝑎 → ¬ 𝑎𝑎)
116114, 115syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎𝑎)
117116orcd 872 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118 ianor 981 . . . . . . . . . . . . . . . . 17 (¬ (𝑎𝑎𝑏 ∈ {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119 opelxp 5670 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎𝑎𝑏 ∈ {𝑏}))
120118, 119xchnxbir 333 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121117, 120sylibr 233 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122 sssucid 6398 . . . . . . . . . . . . . . . . 17 𝑎 ⊆ suc 𝑎
12386sucid 6400 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ suc 𝑏
124 snssi 4769 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑏} ⊆ suc 𝑏
126 xpss12 5649 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127122, 125, 126mp2an 691 . . . . . . . . . . . . . . . 16 (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128 ssdifsn 4749 . . . . . . . . . . . . . . . 16 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129127, 128mpbiran 708 . . . . . . . . . . . . . . 15 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130121, 129sylibr 233 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131 resima2 5973 . . . . . . . . . . . . . 14 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
132130, 131syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
133132sseq1d 3976 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
134112, 133anbi12d 632 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)))
135134rabbidv 3416 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136135inteqd 4913 . . . . . . . . 9 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137 simprr 772 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
138 oveq1 7365 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139138eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140139ralbidv 3175 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑎 → (∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On))
14184, 140ralsn 4643 . . . . . . . . . . . . . . . . 17 (∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
142137, 141sylibr 233 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On)
143 snssi 4769 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → {𝑎} ⊆ On)
144 onss 7720 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → 𝑏 ⊆ On)
145 xpss12 5649 . . . . . . . . . . . . . . . . . . . 20 (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146143, 144, 145syl2an 597 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147146adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
14881fndmi 6607 . . . . . . . . . . . . . . . . . 18 dom +no = (On × On)
149147, 148sseqtrrdi 3996 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150 funimassov 7532 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ ({𝑎} × 𝑏) ⊆ dom +no ) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On))
15183, 149, 150sylancr 588 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On))
152142, 151mpbird 257 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ On)
153 simprl 770 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
154 oveq2 7366 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155154eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
15686, 155ralsn 4643 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157156ralbii 3097 . . . . . . . . . . . . . . . . 17 (∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
158153, 157sylibr 233 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159 onss 7720 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → 𝑎 ⊆ On)
160 snssi 4769 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → {𝑏} ⊆ On)
161 xpss12 5649 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162159, 160, 161syl2an 597 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163162adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164163, 148sseqtrrdi 3996 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165 funimassov 7532 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ (𝑎 × {𝑏}) ⊆ dom +no ) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
16683, 164, 165sylancr 588 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
167158, 166mpbird 257 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ On)
168152, 167unssd 4147 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169 ssorduni 7714 . . . . . . . . . . . . . 14 ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170168, 169syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171 vsnex 5387 . . . . . . . . . . . . . . . . . 18 {𝑎} ∈ V
172171, 86xpex 7688 . . . . . . . . . . . . . . . . 17 ({𝑎} × 𝑏) ∈ V
173 funimaexg 6588 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
17483, 172, 173mp2an 691 . . . . . . . . . . . . . . . 16 ( +no “ ({𝑎} × 𝑏)) ∈ V
175 vsnex 5387 . . . . . . . . . . . . . . . . . 18 {𝑏} ∈ V
17684, 175xpex 7688 . . . . . . . . . . . . . . . . 17 (𝑎 × {𝑏}) ∈ V
177 funimaexg 6588 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
17883, 176, 177mp2an 691 . . . . . . . . . . . . . . . 16 ( +no “ (𝑎 × {𝑏})) ∈ V
179174, 178unex 7681 . . . . . . . . . . . . . . 15 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180179uniex 7679 . . . . . . . . . . . . . 14 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181180elon 6327 . . . . . . . . . . . . 13 ( (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182170, 181sylibr 233 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183 onsucb 7753 . . . . . . . . . . . 12 ( (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
184182, 183sylib 217 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
185 onsucuni 7764 . . . . . . . . . . . . 13 ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
186168, 185syl 17 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
187186unssad 4148 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188186unssbd 4149 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189 sseq2 3971 . . . . . . . . . . . . 13 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190 sseq2 3971 . . . . . . . . . . . . 13 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
191189, 190anbi12d 632 . . . . . . . . . . . 12 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))))
192191rspcev 3582 . . . . . . . . . . 11 ((suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193184, 187, 188, 192syl12anc 836 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194 onintrab2 7733 . . . . . . . . . 10 (∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
195193, 194sylib 217 . . . . . . . . 9 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
196136, 195eqeltrd 2838 . . . . . . . 8 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
19784, 86op1std 7932 . . . . . . . . . . . . . . . 16 (𝑡 = ⟨𝑎, 𝑏⟩ → (1st𝑡) = 𝑎)
198197sneqd 4599 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(1st𝑡)} = {𝑎})
19984, 86op2ndd 7933 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → (2nd𝑡) = 𝑏)
200198, 199xpeq12d 5665 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1st𝑡)} × (2nd𝑡)) = ({𝑎} × 𝑏))
201200imaeq2d 6014 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1st𝑡)} × (2nd𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202201sseq1d 3976 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203199sneqd 4599 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(2nd𝑡)} = {𝑏})
204197, 203xpeq12d 5665 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ((1st𝑡) × {(2nd𝑡)}) = (𝑎 × {𝑏}))
205204imaeq2d 6014 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206205sseq1d 3976 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207202, 206anbi12d 632 . . . . . . . . . . 11 (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208207rabbidv 3416 . . . . . . . . . 10 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209208inteqd 4913 . . . . . . . . 9 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210 imaeq1 6009 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211210sseq1d 3976 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212 imaeq1 6009 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213212sseq1d 3976 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214211, 213anbi12d 632 . . . . . . . . . . 11 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215214rabbidv 3416 . . . . . . . . . 10 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216215inteqd 4913 . . . . . . . . 9 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217 eqid 2737 . . . . . . . . 9 (𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)}) = (𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})
218209, 216, 217ovmpog 7515 . . . . . . . 8 ((⟨𝑎, 𝑏⟩ ∈ 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 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
21980, 91, 196, 218mp3an12i 1466 . . . . . . 7 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))) = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
22079, 219, 1363eqtrd 2781 . . . . . 6 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
221220, 195eqeltrd 2838 . . . . 5 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) ∈ On)
222221, 220jca 513 . . . 4 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}))
223222ex 414 . . 3 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})))
22476, 223syl5 34 . 2 ((𝑎 ∈ 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 “ (𝑎 × {𝑏})) ⊆ 𝑥)})))
22514, 28, 41, 55, 69, 224on2ind 8616 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wral 3065  wrex 3074  {crab 3408  Vcvv 3446  cdif 3908  cun 3909  wss 3911  {csn 4587  cop 4593   cuni 4866   cint 4908   × cxp 5632  dom cdm 5634  cres 5636  cima 5637  Ord word 6317  Oncon0 6318  suc csuc 6320  Fun wfun 6491   Fn wfn 6492  cfv 6497  (class class class)co 7358  cmpo 7360  1st c1st 7920  2nd c2nd 7921   +no cnadd 8612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-frecs 8213  df-nadd 8613
This theorem is referenced by:  naddcl  8624  naddov  8625
  Copyright terms: Public domain W3C validator