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

Theorem naddcllem 8713
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 7438 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
21eleq1d 2824 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3 sneq 4641 . . . . . . . . . 10 (𝑎 = 𝑐 → {𝑎} = {𝑐})
43xpeq1d 5718 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
54imaeq2d 6080 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
65sseq1d 4027 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7 xpeq1 5703 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
87imaeq2d 6080 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
98sseq1d 4027 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
106, 9anbi12d 632 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
1110rabbidv 3441 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
1211inteqd 4956 . . . 4 (𝑎 = 𝑐 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
131, 12eqeq12d 2751 . . 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 7439 . . . 4 (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
1615eleq1d 2824 . . 3 (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17 xpeq2 5710 . . . . . . . . 9 (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
1817imaeq2d 6080 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
1918sseq1d 4027 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20 sneq 4641 . . . . . . . . . 10 (𝑏 = 𝑑 → {𝑏} = {𝑑})
2120xpeq2d 5719 . . . . . . . . 9 (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
2221imaeq2d 6080 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
2322sseq1d 4027 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
2419, 23anbi12d 632 . . . . . 6 (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
2524rabbidv 3441 . . . . 5 (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2625inteqd 4956 . . . 4 (𝑏 = 𝑑 {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2715, 26eqeq12d 2751 . . 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 7438 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
3029eleq1d 2824 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
313xpeq1d 5718 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
3231imaeq2d 6080 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
3332sseq1d 4027 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34 xpeq1 5703 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
3534imaeq2d 6080 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
3635sseq1d 4027 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
3733, 36anbi12d 632 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
3837rabbidv 3441 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
3938inteqd 4956 . . . 4 (𝑎 = 𝑐 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
4029, 39eqeq12d 2751 . . 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 7438 . . . 4 (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
4342eleq1d 2824 . . 3 (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44 sneq 4641 . . . . . . . . . 10 (𝑎 = 𝐴 → {𝑎} = {𝐴})
4544xpeq1d 5718 . . . . . . . . 9 (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
4645imaeq2d 6080 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
4746sseq1d 4027 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48 xpeq1 5703 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
4948imaeq2d 6080 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
5049sseq1d 4027 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
5147, 50anbi12d 632 . . . . . 6 (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
5251rabbidv 3441 . . . . 5 (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5352inteqd 4956 . . . 4 (𝑎 = 𝐴 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5442, 53eqeq12d 2751 . . 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 7439 . . . 4 (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
5756eleq1d 2824 . . 3 (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58 xpeq2 5710 . . . . . . . . 9 (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
5958imaeq2d 6080 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
6059sseq1d 4027 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61 sneq 4641 . . . . . . . . . 10 (𝑏 = 𝐵 → {𝑏} = {𝐵})
6261xpeq2d 5719 . . . . . . . . 9 (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
6362imaeq2d 6080 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
6463sseq1d 4027 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
6560, 64anbi12d 632 . . . . . 6 (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
6665rabbidv 3441 . . . . 5 (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6766inteqd 4956 . . . 4 (𝑏 = 𝐵 {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6856, 67eqeq12d 2751 . . 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 482 . . . . . 6 (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
7170ralimi 3081 . . . . 5 (∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
72713ad2ant2 1133 . . . 4 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
73 simpl 482 . . . . . 6 (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
7473ralimi 3081 . . . . 5 (∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
75743ad2ant3 1134 . . . 4 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
7672, 75jca 511 . . 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 8703 . . . . . . . . 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 8705 . . . . . . . 8 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
7978adantr 480 . . . . . . 7 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
80 opex 5475 . . . . . . . 8 𝑎, 𝑏⟩ ∈ V
81 naddfn 8712 . . . . . . . . . 10 +no Fn (On × On)
82 fnfun 6669 . . . . . . . . . 10 ( +no Fn (On × On) → Fun +no )
8381, 82ax-mp 5 . . . . . . . . 9 Fun +no
84 vex 3482 . . . . . . . . . . . 12 𝑎 ∈ V
8584sucex 7826 . . . . . . . . . . 11 suc 𝑎 ∈ V
86 vex 3482 . . . . . . . . . . . 12 𝑏 ∈ V
8786sucex 7826 . . . . . . . . . . 11 suc 𝑏 ∈ V
8885, 87xpex 7772 . . . . . . . . . 10 (suc 𝑎 × suc 𝑏) ∈ V
8988difexi 5336 . . . . . . . . 9 ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90 resfunexg 7235 . . . . . . . . 9 ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
9183, 89, 90mp2an 692 . . . . . . . 8 ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92 eloni 6396 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ On → Ord 𝑏)
9392ad2antlr 727 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94 ordirr 6404 . . . . . . . . . . . . . . . . . 18 (Ord 𝑏 → ¬ 𝑏𝑏)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏𝑏)
9695olcd 874 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
97 ianor 983 . . . . . . . . . . . . . . . . 17 (¬ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
98 opelxp 5725 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏))
9997, 98xchnxbir 333 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
10096, 99sylibr 234 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
10184sucid 6468 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ suc 𝑎
102 snssi 4813 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑎} ⊆ suc 𝑎
104 sssucid 6466 . . . . . . . . . . . . . . . . 17 𝑏 ⊆ suc 𝑏
105 xpss12 5704 . . . . . . . . . . . . . . . . 17 (({𝑎} ⊆ suc 𝑎𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106103, 104, 105mp2an 692 . . . . . . . . . . . . . . . 16 ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107 ssdifsn 4793 . . . . . . . . . . . . . . . 16 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108106, 107mpbiran 709 . . . . . . . . . . . . . . 15 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109100, 108sylibr 234 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110 resima2 6036 . . . . . . . . . . . . . 14 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
111109, 110syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
112111sseq1d 4027 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113 eloni 6396 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ On → Ord 𝑎)
114113ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115 ordirr 6404 . . . . . . . . . . . . . . . . . 18 (Ord 𝑎 → ¬ 𝑎𝑎)
116114, 115syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎𝑎)
117116orcd 873 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118 ianor 983 . . . . . . . . . . . . . . . . 17 (¬ (𝑎𝑎𝑏 ∈ {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119 opelxp 5725 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎𝑎𝑏 ∈ {𝑏}))
120118, 119xchnxbir 333 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121117, 120sylibr 234 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122 sssucid 6466 . . . . . . . . . . . . . . . . 17 𝑎 ⊆ suc 𝑎
12386sucid 6468 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ suc 𝑏
124 snssi 4813 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑏} ⊆ suc 𝑏
126 xpss12 5704 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127122, 125, 126mp2an 692 . . . . . . . . . . . . . . . 16 (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128 ssdifsn 4793 . . . . . . . . . . . . . . . 16 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129127, 128mpbiran 709 . . . . . . . . . . . . . . 15 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130121, 129sylibr 234 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131 resima2 6036 . . . . . . . . . . . . . 14 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
132130, 131syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
133132sseq1d 4027 . . . . . . . . . . . 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 3441 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136135inteqd 4956 . . . . . . . . 9 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137 simprr 773 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
138 oveq1 7438 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139138eleq1d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140139ralbidv 3176 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑎 → (∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On))
14184, 140ralsn 4686 . . . . . . . . . . . . . . . . 17 (∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
142137, 141sylibr 234 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On)
143 snssi 4813 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → {𝑎} ⊆ On)
144 onss 7804 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → 𝑏 ⊆ On)
145 xpss12 5704 . . . . . . . . . . . . . . . . . . . 20 (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146143, 144, 145syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147146adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
14881fndmi 6673 . . . . . . . . . . . . . . . . . 18 dom +no = (On × On)
149147, 148sseqtrrdi 4047 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150 funimassov 7610 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ ({𝑎} × 𝑏) ⊆ dom +no ) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On))
15183, 149, 150sylancr 587 . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
154 oveq2 7439 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155154eleq1d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
15686, 155ralsn 4686 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157156ralbii 3091 . . . . . . . . . . . . . . . . 17 (∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
158153, 157sylibr 234 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159 onss 7804 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → 𝑎 ⊆ On)
160 snssi 4813 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → {𝑏} ⊆ On)
161 xpss12 5704 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162159, 160, 161syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163162adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164163, 148sseqtrrdi 4047 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165 funimassov 7610 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ (𝑎 × {𝑏}) ⊆ dom +no ) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
16683, 164, 165sylancr 587 . . . . . . . . . . . . . . . 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 4202 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169 ssorduni 7798 . . . . . . . . . . . . . 14 ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170168, 169syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171 vsnex 5440 . . . . . . . . . . . . . . . . . 18 {𝑎} ∈ V
172171, 86xpex 7772 . . . . . . . . . . . . . . . . 17 ({𝑎} × 𝑏) ∈ V
173 funimaexg 6654 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
17483, 172, 173mp2an 692 . . . . . . . . . . . . . . . 16 ( +no “ ({𝑎} × 𝑏)) ∈ V
175 vsnex 5440 . . . . . . . . . . . . . . . . . 18 {𝑏} ∈ V
17684, 175xpex 7772 . . . . . . . . . . . . . . . . 17 (𝑎 × {𝑏}) ∈ V
177 funimaexg 6654 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
17883, 176, 177mp2an 692 . . . . . . . . . . . . . . . 16 ( +no “ (𝑎 × {𝑏})) ∈ V
179174, 178unex 7763 . . . . . . . . . . . . . . 15 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180179uniex 7760 . . . . . . . . . . . . . 14 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181180elon 6395 . . . . . . . . . . . . 13 ( (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182170, 181sylibr 234 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183 onsucb 7837 . . . . . . . . . . . 12 ( (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
184182, 183sylib 218 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
185 onsucuni 7848 . . . . . . . . . . . . 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 4203 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188186unssbd 4204 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189 sseq2 4022 . . . . . . . . . . . . 13 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190 sseq2 4022 . . . . . . . . . . . . 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 3622 . . . . . . . . . . 11 ((suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193184, 187, 188, 192syl12anc 837 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194 onintrab2 7817 . . . . . . . . . 10 (∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
195193, 194sylib 218 . . . . . . . . 9 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
196136, 195eqeltrd 2839 . . . . . . . 8 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
19784, 86op1std 8023 . . . . . . . . . . . . . . . 16 (𝑡 = ⟨𝑎, 𝑏⟩ → (1st𝑡) = 𝑎)
198197sneqd 4643 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(1st𝑡)} = {𝑎})
19984, 86op2ndd 8024 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → (2nd𝑡) = 𝑏)
200198, 199xpeq12d 5720 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1st𝑡)} × (2nd𝑡)) = ({𝑎} × 𝑏))
201200imaeq2d 6080 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1st𝑡)} × (2nd𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202201sseq1d 4027 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203199sneqd 4643 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(2nd𝑡)} = {𝑏})
204197, 203xpeq12d 5720 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ((1st𝑡) × {(2nd𝑡)}) = (𝑎 × {𝑏}))
205204imaeq2d 6080 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206205sseq1d 4027 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207202, 206anbi12d 632 . . . . . . . . . . 11 (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208207rabbidv 3441 . . . . . . . . . 10 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209208inteqd 4956 . . . . . . . . 9 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210 imaeq1 6075 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211210sseq1d 4027 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212 imaeq1 6075 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213212sseq1d 4027 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214211, 213anbi12d 632 . . . . . . . . . . 11 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215214rabbidv 3441 . . . . . . . . . 10 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216215inteqd 4956 . . . . . . . . 9 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217 eqid 2735 . . . . . . . . 9 (𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)}) = (𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})
218209, 216, 217ovmpog 7592 . . . . . . . 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 1464 . . . . . . 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 2779 . . . . . 6 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
221220, 195eqeltrd 2839 . . . . 5 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) ∈ On)
222221, 220jca 511 . . . 4 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}))
223222ex 412 . . 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 8706 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  cdif 3960  cun 3961  wss 3963  {csn 4631  cop 4637   cuni 4912   cint 4951   × cxp 5687  dom cdm 5689  cres 5691  cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388  Fun wfun 6557   Fn wfn 6558  cfv 6563  (class class class)co 7431  cmpo 7433  1st c1st 8011  2nd c2nd 8012   +no cnadd 8702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-frecs 8305  df-nadd 8703
This theorem is referenced by:  naddcl  8714  naddov  8715
  Copyright terms: Public domain W3C validator