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

Theorem naddcllem 8622
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 7364 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
21eleq1d 2822 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3 sneq 4596 . . . . . . . . . 10 (𝑎 = 𝑐 → {𝑎} = {𝑐})
43xpeq1d 5662 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
54imaeq2d 6013 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
65sseq1d 3975 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7 xpeq1 5647 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
87imaeq2d 6013 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
98sseq1d 3975 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
106, 9anbi12d 631 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
1110rabbidv 3415 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
1211inteqd 4912 . . . 4 (𝑎 = 𝑐 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
131, 12eqeq12d 2752 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}))
142, 13anbi12d 631 . 2 (𝑎 = 𝑐 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})))
15 oveq2 7365 . . . 4 (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
1615eleq1d 2822 . . 3 (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17 xpeq2 5654 . . . . . . . . 9 (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
1817imaeq2d 6013 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
1918sseq1d 3975 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20 sneq 4596 . . . . . . . . . 10 (𝑏 = 𝑑 → {𝑏} = {𝑑})
2120xpeq2d 5663 . . . . . . . . 9 (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
2221imaeq2d 6013 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
2322sseq1d 3975 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
2419, 23anbi12d 631 . . . . . 6 (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
2524rabbidv 3415 . . . . 5 (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2625inteqd 4912 . . . 4 (𝑏 = 𝑑 {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2715, 26eqeq12d 2752 . . 3 (𝑏 = 𝑑 → ((𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
2816, 27anbi12d 631 . 2 (𝑏 = 𝑑 → (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
29 oveq1 7364 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
3029eleq1d 2822 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
313xpeq1d 5662 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
3231imaeq2d 6013 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
3332sseq1d 3975 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34 xpeq1 5647 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
3534imaeq2d 6013 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
3635sseq1d 3975 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
3733, 36anbi12d 631 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
3837rabbidv 3415 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
3938inteqd 4912 . . . 4 (𝑎 = 𝑐 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
4029, 39eqeq12d 2752 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
4130, 40anbi12d 631 . 2 (𝑎 = 𝑐 → (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
42 oveq1 7364 . . . 4 (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
4342eleq1d 2822 . . 3 (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44 sneq 4596 . . . . . . . . . 10 (𝑎 = 𝐴 → {𝑎} = {𝐴})
4544xpeq1d 5662 . . . . . . . . 9 (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
4645imaeq2d 6013 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
4746sseq1d 3975 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48 xpeq1 5647 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
4948imaeq2d 6013 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
5049sseq1d 3975 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
5147, 50anbi12d 631 . . . . . 6 (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
5251rabbidv 3415 . . . . 5 (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5352inteqd 4912 . . . 4 (𝑎 = 𝐴 {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5442, 53eqeq12d 2752 . . 3 (𝑎 = 𝐴 → ((𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}))
5543, 54anbi12d 631 . 2 (𝑎 = 𝐴 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})))
56 oveq2 7365 . . . 4 (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
5756eleq1d 2822 . . 3 (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58 xpeq2 5654 . . . . . . . . 9 (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
5958imaeq2d 6013 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
6059sseq1d 3975 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61 sneq 4596 . . . . . . . . . 10 (𝑏 = 𝐵 → {𝑏} = {𝐵})
6261xpeq2d 5663 . . . . . . . . 9 (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
6362imaeq2d 6013 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
6463sseq1d 3975 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
6560, 64anbi12d 631 . . . . . 6 (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
6665rabbidv 3415 . . . . 5 (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6766inteqd 4912 . . . 4 (𝑏 = 𝐵 {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6856, 67eqeq12d 2752 . . 3 (𝑏 = 𝐵 → ((𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
6957, 68anbi12d 631 . 2 (𝑏 = 𝐵 → (((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})))
70 simpl 483 . . . . . 6 (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
7170ralimi 3086 . . . . 5 (∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
72713ad2ant2 1134 . . . 4 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
73 simpl 483 . . . . . 6 (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
7473ralimi 3086 . . . . 5 (∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
75743ad2ant3 1135 . . . 4 ((∀𝑐𝑎𝑑𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
7672, 75jca 512 . . 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 8612 . . . . . . . . 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 8614 . . . . . . . 8 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
7978adantr 481 . . . . . . 7 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
80 opex 5421 . . . . . . . 8 𝑎, 𝑏⟩ ∈ V
81 naddfn 8621 . . . . . . . . . 10 +no Fn (On × On)
82 fnfun 6602 . . . . . . . . . 10 ( +no Fn (On × On) → Fun +no )
8381, 82ax-mp 5 . . . . . . . . 9 Fun +no
84 vex 3449 . . . . . . . . . . . 12 𝑎 ∈ V
8584sucex 7741 . . . . . . . . . . 11 suc 𝑎 ∈ V
86 vex 3449 . . . . . . . . . . . 12 𝑏 ∈ V
8786sucex 7741 . . . . . . . . . . 11 suc 𝑏 ∈ V
8885, 87xpex 7687 . . . . . . . . . 10 (suc 𝑎 × suc 𝑏) ∈ V
8988difexi 5285 . . . . . . . . 9 ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90 resfunexg 7165 . . . . . . . . 9 ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
9183, 89, 90mp2an 690 . . . . . . . 8 ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92 eloni 6327 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ On → Ord 𝑏)
9392ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94 ordirr 6335 . . . . . . . . . . . . . . . . . 18 (Ord 𝑏 → ¬ 𝑏𝑏)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏𝑏)
9695olcd 872 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
97 ianor 980 . . . . . . . . . . . . . . . . 17 (¬ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
98 opelxp 5669 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏))
9997, 98xchnxbir 332 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
10096, 99sylibr 233 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
10184sucid 6399 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ suc 𝑎
102 snssi 4768 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑎} ⊆ suc 𝑎
104 sssucid 6397 . . . . . . . . . . . . . . . . 17 𝑏 ⊆ suc 𝑏
105 xpss12 5648 . . . . . . . . . . . . . . . . 17 (({𝑎} ⊆ suc 𝑎𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106103, 104, 105mp2an 690 . . . . . . . . . . . . . . . 16 ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107 ssdifsn 4748 . . . . . . . . . . . . . . . 16 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108106, 107mpbiran 707 . . . . . . . . . . . . . . 15 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109100, 108sylibr 233 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110 resima2 5972 . . . . . . . . . . . . . 14 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
111109, 110syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
112111sseq1d 3975 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113 eloni 6327 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ On → Ord 𝑎)
114113ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115 ordirr 6335 . . . . . . . . . . . . . . . . . 18 (Ord 𝑎 → ¬ 𝑎𝑎)
116114, 115syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎𝑎)
117116orcd 871 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118 ianor 980 . . . . . . . . . . . . . . . . 17 (¬ (𝑎𝑎𝑏 ∈ {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119 opelxp 5669 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎𝑎𝑏 ∈ {𝑏}))
120118, 119xchnxbir 332 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121117, 120sylibr 233 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122 sssucid 6397 . . . . . . . . . . . . . . . . 17 𝑎 ⊆ suc 𝑎
12386sucid 6399 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ suc 𝑏
124 snssi 4768 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑏} ⊆ suc 𝑏
126 xpss12 5648 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127122, 125, 126mp2an 690 . . . . . . . . . . . . . . . 16 (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128 ssdifsn 4748 . . . . . . . . . . . . . . . 16 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129127, 128mpbiran 707 . . . . . . . . . . . . . . 15 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130121, 129sylibr 233 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131 resima2 5972 . . . . . . . . . . . . . 14 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
132130, 131syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
133132sseq1d 3975 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
134112, 133anbi12d 631 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)))
135134rabbidv 3415 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136135inteqd 4912 . . . . . . . . 9 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
138 oveq1 7364 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139138eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140139ralbidv 3174 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑎 → (∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On))
14184, 140ralsn 4642 . . . . . . . . . . . . . . . . 17 (∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
142137, 141sylibr 233 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On)
143 snssi 4768 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → {𝑎} ⊆ On)
144 onss 7719 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → 𝑏 ⊆ On)
145 xpss12 5648 . . . . . . . . . . . . . . . . . . . 20 (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146143, 144, 145syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147146adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
14881fndmi 6606 . . . . . . . . . . . . . . . . . 18 dom +no = (On × On)
149147, 148sseqtrrdi 3995 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150 funimassov 7531 . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ On)
153 simprl 769 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
154 oveq2 7365 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155154eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
15686, 155ralsn 4642 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157156ralbii 3096 . . . . . . . . . . . . . . . . 17 (∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
158153, 157sylibr 233 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159 onss 7719 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → 𝑎 ⊆ On)
160 snssi 4768 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → {𝑏} ⊆ On)
161 xpss12 5648 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162159, 160, 161syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163162adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164163, 148sseqtrrdi 3995 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165 funimassov 7531 . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ On)
168152, 167unssd 4146 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169 ssorduni 7713 . . . . . . . . . . . . . 14 ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170168, 169syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171 vsnex 5386 . . . . . . . . . . . . . . . . . 18 {𝑎} ∈ V
172171, 86xpex 7687 . . . . . . . . . . . . . . . . 17 ({𝑎} × 𝑏) ∈ V
173 funimaexg 6587 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
17483, 172, 173mp2an 690 . . . . . . . . . . . . . . . 16 ( +no “ ({𝑎} × 𝑏)) ∈ V
175 vsnex 5386 . . . . . . . . . . . . . . . . . 18 {𝑏} ∈ V
17684, 175xpex 7687 . . . . . . . . . . . . . . . . 17 (𝑎 × {𝑏}) ∈ V
177 funimaexg 6587 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
17883, 176, 177mp2an 690 . . . . . . . . . . . . . . . 16 ( +no “ (𝑎 × {𝑏})) ∈ V
179174, 178unex 7680 . . . . . . . . . . . . . . 15 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180179uniex 7678 . . . . . . . . . . . . . 14 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181180elon 6326 . . . . . . . . . . . . 13 ( (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182170, 181sylibr 233 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183 onsucb 7752 . . . . . . . . . . . 12 ( (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
184182, 183sylib 217 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
185 onsucuni 7763 . . . . . . . . . . . . 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 4147 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188186unssbd 4148 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189 sseq2 3970 . . . . . . . . . . . . 13 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190 sseq2 3970 . . . . . . . . . . . . 13 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
191189, 190anbi12d 631 . . . . . . . . . . . 12 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))))
192191rspcev 3581 . . . . . . . . . . 11 ((suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193184, 187, 188, 192syl12anc 835 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194 onintrab2 7732 . . . . . . . . . 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 7931 . . . . . . . . . . . . . . . 16 (𝑡 = ⟨𝑎, 𝑏⟩ → (1st𝑡) = 𝑎)
198197sneqd 4598 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(1st𝑡)} = {𝑎})
19984, 86op2ndd 7932 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → (2nd𝑡) = 𝑏)
200198, 199xpeq12d 5664 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1st𝑡)} × (2nd𝑡)) = ({𝑎} × 𝑏))
201200imaeq2d 6013 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1st𝑡)} × (2nd𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202201sseq1d 3975 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203199sneqd 4598 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(2nd𝑡)} = {𝑏})
204197, 203xpeq12d 5664 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ((1st𝑡) × {(2nd𝑡)}) = (𝑎 × {𝑏}))
205204imaeq2d 6013 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206205sseq1d 3975 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207202, 206anbi12d 631 . . . . . . . . . . 11 (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208207rabbidv 3415 . . . . . . . . . 10 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209208inteqd 4912 . . . . . . . . 9 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210 imaeq1 6008 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211210sseq1d 3975 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212 imaeq1 6008 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213212sseq1d 3975 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214211, 213anbi12d 631 . . . . . . . . . . 11 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215214rabbidv 3415 . . . . . . . . . 10 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216215inteqd 4912 . . . . . . . . 9 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217 eqid 2736 . . . . . . . . 9 (𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)}) = (𝑡 ∈ V, 𝑓 ∈ V ↦ {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)})
218209, 216, 217ovmpog 7514 . . . . . . . 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 1465 . . . . . . 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 2780 . . . . . 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 512 . . . 4 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}))
223222ex 413 . . 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 8615 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  wss 3910  {csn 4586  cop 4592   cuni 4865   cint 4907   × cxp 5631  dom cdm 5633  cres 5635  cima 5636  Ord word 6316  Oncon0 6317  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  cfv 6496  (class class class)co 7357  cmpo 7359  1st c1st 7919  2nd c2nd 7920   +no cnadd 8611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-frecs 8212  df-nadd 8612
This theorem is referenced by:  naddcl  8623  naddov  8624
  Copyright terms: Public domain W3C validator