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

Theorem naddcllem 8714
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 2826 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3 sneq 4636 . . . . . . . . . 10 (𝑎 = 𝑐 → {𝑎} = {𝑐})
43xpeq1d 5714 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
54imaeq2d 6078 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
65sseq1d 4015 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7 xpeq1 5699 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
87imaeq2d 6078 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
98sseq1d 4015 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
106, 9anbi12d 632 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
1110rabbidv 3444 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
1211inteqd 4951 . . . 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 7439 . . . 4 (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
1615eleq1d 2826 . . 3 (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17 xpeq2 5706 . . . . . . . . 9 (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
1817imaeq2d 6078 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
1918sseq1d 4015 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20 sneq 4636 . . . . . . . . . 10 (𝑏 = 𝑑 → {𝑏} = {𝑑})
2120xpeq2d 5715 . . . . . . . . 9 (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
2221imaeq2d 6078 . . . . . . . 8 (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
2322sseq1d 4015 . . . . . . 7 (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
2419, 23anbi12d 632 . . . . . 6 (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
2524rabbidv 3444 . . . . 5 (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
2625inteqd 4951 . . . 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 7438 . . . 4 (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
3029eleq1d 2826 . . 3 (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
313xpeq1d 5714 . . . . . . . . 9 (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
3231imaeq2d 6078 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
3332sseq1d 4015 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34 xpeq1 5699 . . . . . . . . 9 (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
3534imaeq2d 6078 . . . . . . . 8 (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
3635sseq1d 4015 . . . . . . 7 (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
3733, 36anbi12d 632 . . . . . 6 (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
3837rabbidv 3444 . . . . 5 (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
3938inteqd 4951 . . . 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 7438 . . . 4 (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
4342eleq1d 2826 . . 3 (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44 sneq 4636 . . . . . . . . . 10 (𝑎 = 𝐴 → {𝑎} = {𝐴})
4544xpeq1d 5714 . . . . . . . . 9 (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
4645imaeq2d 6078 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
4746sseq1d 4015 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48 xpeq1 5699 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
4948imaeq2d 6078 . . . . . . . 8 (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
5049sseq1d 4015 . . . . . . 7 (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
5147, 50anbi12d 632 . . . . . 6 (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
5251rabbidv 3444 . . . . 5 (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
5352inteqd 4951 . . . 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 7439 . . . 4 (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
5756eleq1d 2826 . . 3 (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58 xpeq2 5706 . . . . . . . . 9 (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
5958imaeq2d 6078 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
6059sseq1d 4015 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61 sneq 4636 . . . . . . . . . 10 (𝑏 = 𝐵 → {𝑏} = {𝐵})
6261xpeq2d 5715 . . . . . . . . 9 (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
6362imaeq2d 6078 . . . . . . . 8 (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
6463sseq1d 4015 . . . . . . 7 (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
6560, 64anbi12d 632 . . . . . 6 (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
6665rabbidv 3444 . . . . 5 (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
6766inteqd 4951 . . . 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 482 . . . . . 6 (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
7170ralimi 3083 . . . . 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 482 . . . . . 6 (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
7473ralimi 3083 . . . . 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 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 8704 . . . . . . . . 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 8706 . . . . . . . 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 5469 . . . . . . . 8 𝑎, 𝑏⟩ ∈ V
81 naddfn 8713 . . . . . . . . . 10 +no Fn (On × On)
82 fnfun 6668 . . . . . . . . . 10 ( +no Fn (On × On) → Fun +no )
8381, 82ax-mp 5 . . . . . . . . 9 Fun +no
84 vex 3484 . . . . . . . . . . . 12 𝑎 ∈ V
8584sucex 7826 . . . . . . . . . . 11 suc 𝑎 ∈ V
86 vex 3484 . . . . . . . . . . . 12 𝑏 ∈ V
8786sucex 7826 . . . . . . . . . . 11 suc 𝑏 ∈ V
8885, 87xpex 7773 . . . . . . . . . 10 (suc 𝑎 × suc 𝑏) ∈ V
8988difexi 5330 . . . . . . . . 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 6394 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ On → Ord 𝑏)
9392ad2antlr 727 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94 ordirr 6402 . . . . . . . . . . . . . . . . . 18 (Ord 𝑏 → ¬ 𝑏𝑏)
9593, 94syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏𝑏)
9695olcd 875 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
97 ianor 984 . . . . . . . . . . . . . . . . 17 (¬ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
98 opelxp 5721 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏𝑏))
9997, 98xchnxbir 333 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏𝑏))
10096, 99sylibr 234 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
10184sucid 6466 . . . . . . . . . . . . . . . . . 18 𝑎 ∈ suc 𝑎
102 snssi 4808 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑎} ⊆ suc 𝑎
104 sssucid 6464 . . . . . . . . . . . . . . . . 17 𝑏 ⊆ suc 𝑏
105 xpss12 5700 . . . . . . . . . . . . . . . . 17 (({𝑎} ⊆ suc 𝑎𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106103, 104, 105mp2an 692 . . . . . . . . . . . . . . . 16 ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107 ssdifsn 4788 . . . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . 14 (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
111109, 110syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
112111sseq1d 4015 . . . . . . . . . . . 12 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113 eloni 6394 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ On → Ord 𝑎)
114113ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115 ordirr 6402 . . . . . . . . . . . . . . . . . 18 (Ord 𝑎 → ¬ 𝑎𝑎)
116114, 115syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎𝑎)
117116orcd 874 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118 ianor 984 . . . . . . . . . . . . . . . . 17 (¬ (𝑎𝑎𝑏 ∈ {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119 opelxp 5721 . . . . . . . . . . . . . . . . 17 (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎𝑎𝑏 ∈ {𝑏}))
120118, 119xchnxbir 333 . . . . . . . . . . . . . . . 16 (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121117, 120sylibr 234 . . . . . . . . . . . . . . 15 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122 sssucid 6464 . . . . . . . . . . . . . . . . 17 𝑎 ⊆ suc 𝑎
12386sucid 6466 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ suc 𝑏
124 snssi 4808 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑏} ⊆ suc 𝑏
126 xpss12 5700 . . . . . . . . . . . . . . . . 17 ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127122, 125, 126mp2an 692 . . . . . . . . . . . . . . . 16 (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128 ssdifsn 4788 . . . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . 14 ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
132130, 131syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
133132sseq1d 4015 . . . . . . . . . . . 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 3444 . . . . . . . . . 10 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136135inteqd 4951 . . . . . . . . 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 2826 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140139ralbidv 3178 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑎 → (∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On))
14184, 140ralsn 4681 . . . . . . . . . . . . . . . . 17 (∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)
142137, 141sylibr 234 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑𝑏 (𝑡 +no 𝑑) ∈ On)
143 snssi 4808 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → {𝑎} ⊆ On)
144 onss 7805 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → 𝑏 ⊆ On)
145 xpss12 5700 . . . . . . . . . . . . . . . . . . . 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 6672 . . . . . . . . . . . . . . . . . 18 dom +no = (On × On)
149147, 148sseqtrrdi 4025 . . . . . . . . . . . . . . . . 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 2826 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
15686, 155ralsn 4681 . . . . . . . . . . . . . . . . . 18 (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157156ralbii 3093 . . . . . . . . . . . . . . . . 17 (∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On)
158153, 157sylibr 234 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐𝑎𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159 onss 7805 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ On → 𝑎 ⊆ On)
160 snssi 4808 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ On → {𝑏} ⊆ On)
161 xpss12 5700 . . . . . . . . . . . . . . . . . . . 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 4025 . . . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . 14 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169 ssorduni 7799 . . . . . . . . . . . . . 14 ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170168, 169syl 17 . . . . . . . . . . . . 13 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171 vsnex 5434 . . . . . . . . . . . . . . . . . 18 {𝑎} ∈ V
172171, 86xpex 7773 . . . . . . . . . . . . . . . . 17 ({𝑎} × 𝑏) ∈ V
173 funimaexg 6653 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
17483, 172, 173mp2an 692 . . . . . . . . . . . . . . . 16 ( +no “ ({𝑎} × 𝑏)) ∈ V
175 vsnex 5434 . . . . . . . . . . . . . . . . . 18 {𝑏} ∈ V
17684, 175xpex 7773 . . . . . . . . . . . . . . . . 17 (𝑎 × {𝑏}) ∈ V
177 funimaexg 6653 . . . . . . . . . . . . . . . . 17 ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
17883, 176, 177mp2an 692 . . . . . . . . . . . . . . . 16 ( +no “ (𝑎 × {𝑏})) ∈ V
179174, 178unex 7764 . . . . . . . . . . . . . . 15 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180179uniex 7761 . . . . . . . . . . . . . 14 (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181180elon 6393 . . . . . . . . . . . . 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 4193 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188186unssbd 4194 . . . . . . . . . . 11 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189 sseq2 4010 . . . . . . . . . . . . 13 (𝑥 = suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190 sseq2 4010 . . . . . . . . . . . . 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 2841 . . . . . . . 8 (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
19784, 86op1std 8024 . . . . . . . . . . . . . . . 16 (𝑡 = ⟨𝑎, 𝑏⟩ → (1st𝑡) = 𝑎)
198197sneqd 4638 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(1st𝑡)} = {𝑎})
19984, 86op2ndd 8025 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → (2nd𝑡) = 𝑏)
200198, 199xpeq12d 5716 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1st𝑡)} × (2nd𝑡)) = ({𝑎} × 𝑏))
201200imaeq2d 6078 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1st𝑡)} × (2nd𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202201sseq1d 4015 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203199sneqd 4638 . . . . . . . . . . . . . . 15 (𝑡 = ⟨𝑎, 𝑏⟩ → {(2nd𝑡)} = {𝑏})
204197, 203xpeq12d 5716 . . . . . . . . . . . . . 14 (𝑡 = ⟨𝑎, 𝑏⟩ → ((1st𝑡) × {(2nd𝑡)}) = (𝑎 × {𝑏}))
205204imaeq2d 6078 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206205sseq1d 4015 . . . . . . . . . . . 12 (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207202, 206anbi12d 632 . . . . . . . . . . 11 (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208207rabbidv 3444 . . . . . . . . . 10 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209208inteqd 4951 . . . . . . . . 9 (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1st𝑡)} × (2nd𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1st𝑡) × {(2nd𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210 imaeq1 6073 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211210sseq1d 4015 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212 imaeq1 6073 . . . . . . . . . . . . 13 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213212sseq1d 4015 . . . . . . . . . . . 12 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214211, 213anbi12d 632 . . . . . . . . . . 11 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215214rabbidv 3444 . . . . . . . . . 10 (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216215inteqd 4951 . . . . . . . . 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 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 1467 . . . . . . 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 2841 . . . . 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 8707 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 848  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  wss 3951  {csn 4626  cop 4632   cuni 4907   cint 4946   × cxp 5683  dom cdm 5685  cres 5687  cima 5688  Ord word 6383  Oncon0 6384  suc csuc 6386  Fun wfun 6555   Fn wfn 6556  cfv 6561  (class class class)co 7431  cmpo 7433  1st c1st 8012  2nd c2nd 8013   +no cnadd 8703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-frecs 8306  df-nadd 8704
This theorem is referenced by:  naddcl  8715  naddov  8716
  Copyright terms: Public domain W3C validator