Theorem naddunif 8680

Description: Uniformity theorem for natural addition. If 𝐴 is the upper bound of 𝑋 and 𝐵 is the upper bound of 𝑌, then (𝐴 +no 𝐵) can be expressed in terms of 𝑋 and 𝑌. (Contributed by Scott Fenton, 20-Jan-2025.)

Hypotheses

Ref	Expression
naddunif.1	⊢ (𝜑 → 𝐴 ∈ On)
naddunif.2	⊢ (𝜑 → 𝐵 ∈ On)
naddunif.3	⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})
naddunif.4	⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦})

Assertion

Ref	Expression
naddunif	⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})

Distinct variable groups:   𝑥,𝐴,𝑧   𝑧,𝐵,𝑦   𝑥,𝑋,𝑧   𝑧,𝑌,𝑦   𝜑,𝑥   𝜑,𝑦,𝑧

Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑥)   𝑋(𝑦)   𝑌(𝑥)

Proof of Theorem naddunif

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑟 𝑠 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		naddunif.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
2		naddunif.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ On)
3		naddov3 8667	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
4	1, 2, 3	syl2anc 595	. 2 ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
5		naddfn 8661	. . . . . . 7 ⊢ +no Fn (On × On)
6		fnfun 6636	. . . . . . 7 ⊢ ( +no Fn (On × On) → Fun +no )
7	5, 6	ax-mp 5	. . . . . 6 ⊢ Fun +no
8		snex 5411	. . . . . . 7 ⊢ {𝐴} ∈ V
9		xpexg 7749	. . . . . . 7 ⊢ (({𝐴} ∈ V ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ∈ V)
10	8, 2, 9	sylancr 598	. . . . . 6 ⊢ (𝜑 → ({𝐴} × 𝐵) ∈ V)
11		funimaexg 6623	. . . . . 6 ⊢ ((Fun +no ∧ ({𝐴} × 𝐵) ∈ V) → ( +no “ ({𝐴} × 𝐵)) ∈ V)
12	7, 10, 11	sylancr 598	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ V)
13		imassrn 6074	. . . . . . 7 ⊢ ( +no “ ({𝐴} × 𝐵)) ⊆ ran +no
14		naddf 8668	. . . . . . . 8 ⊢ +no :(On × On)⟶On
15		frn 6714	. . . . . . . 8 ⊢ ( +no :(On × On)⟶On → ran +no ⊆ On)
16	14, 15	ax-mp 5	. . . . . . 7 ⊢ ran +no ⊆ On
17	13, 16	sstri 3952	. . . . . 6 ⊢ ( +no “ ({𝐴} × 𝐵)) ⊆ On
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ⊆ On)
19	12, 18	elpwd 4571	. . . 4 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On)
20		snex 5411	. . . . . . 7 ⊢ {𝐵} ∈ V
21		xpexg 7749	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ {𝐵} ∈ V) → (𝐴 × {𝐵}) ∈ V)
22	1, 20, 21	sylancl 597	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ V)
23		funimaexg 6623	. . . . . 6 ⊢ ((Fun +no ∧ (𝐴 × {𝐵}) ∈ V) → ( +no “ (𝐴 × {𝐵})) ∈ V)
24	7, 22, 23	sylancr 598	. . . . 5 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ V)
25		imassrn 6074	. . . . . . 7 ⊢ ( +no “ (𝐴 × {𝐵})) ⊆ ran +no
26	25, 16	sstri 3952	. . . . . 6 ⊢ ( +no “ (𝐴 × {𝐵})) ⊆ On
27	26	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ⊆ On)
28	24, 27	elpwd 4571	. . . 4 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On)
29		pwuncl 7769	. . . 4 ⊢ ((( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On ∧ ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On) → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
30	19, 28, 29	syl2anc 595	. . 3 ⊢ (𝜑 → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
31		naddunif.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})
32	31, 1	eqeltrrd 2870	. . . . . . . . 9 ⊢ (𝜑 → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ∈ On)
33		onintrab2 7796	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 ↔ ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ∈ On)
34	32, 33	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ On 𝑋 ⊆ 𝑥)
35		vex 3465	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
36	35	ssex 5292	. . . . . . . . 9 ⊢ (𝑋 ⊆ 𝑥 → 𝑋 ∈ V)
37	36	rexlimivw 3168	. . . . . . . 8 ⊢ (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 → 𝑋 ∈ V)
38	34, 37	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ V)
39		xpexg 7749	. . . . . . 7 ⊢ ((𝑋 ∈ V ∧ {𝐵} ∈ V) → (𝑋 × {𝐵}) ∈ V)
40	38, 20, 39	sylancl 597	. . . . . 6 ⊢ (𝜑 → (𝑋 × {𝐵}) ∈ V)
41		funimaexg 6623	. . . . . 6 ⊢ ((Fun +no ∧ (𝑋 × {𝐵}) ∈ V) → ( +no “ (𝑋 × {𝐵})) ∈ V)
42	7, 40, 41	sylancr 598	. . . . 5 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ V)
43		imassrn 6074	. . . . . . 7 ⊢ ( +no “ (𝑋 × {𝐵})) ⊆ ran +no
44	43, 16	sstri 3952	. . . . . 6 ⊢ ( +no “ (𝑋 × {𝐵})) ⊆ On
45	44	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ⊆ On)
46	42, 45	elpwd 4571	. . . 4 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On)
47		naddunif.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦})
48	47, 2	eqeltrrd 2870	. . . . . . . . 9 ⊢ (𝜑 → ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦} ∈ On)
49		onintrab2 7796	. . . . . . . . 9 ⊢ (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 ↔ ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦} ∈ On)
50	48, 49	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → ∃𝑦 ∈ On 𝑌 ⊆ 𝑦)
51		vex 3465	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
52	51	ssex 5292	. . . . . . . . 9 ⊢ (𝑌 ⊆ 𝑦 → 𝑌 ∈ V)
53	52	rexlimivw 3168	. . . . . . . 8 ⊢ (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 → 𝑌 ∈ V)
54	50, 53	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ V)
55		xpexg 7749	. . . . . . 7 ⊢ (({𝐴} ∈ V ∧ 𝑌 ∈ V) → ({𝐴} × 𝑌) ∈ V)
56	8, 54, 55	sylancr 598	. . . . . 6 ⊢ (𝜑 → ({𝐴} × 𝑌) ∈ V)
57		funimaexg 6623	. . . . . 6 ⊢ ((Fun +no ∧ ({𝐴} × 𝑌) ∈ V) → ( +no “ ({𝐴} × 𝑌)) ∈ V)
58	7, 56, 57	sylancr 598	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ V)
59		imassrn 6074	. . . . . . 7 ⊢ ( +no “ ({𝐴} × 𝑌)) ⊆ ran +no
60	59, 16	sstri 3952	. . . . . 6 ⊢ ( +no “ ({𝐴} × 𝑌)) ⊆ On
61	60	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ⊆ On)
62	58, 61	elpwd 4571	. . . 4 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On)
63		pwuncl 7769	. . . 4 ⊢ ((( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On ∧ ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On) → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
64	46, 62, 63	syl2anc 595	. . 3 ⊢ (𝜑 → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
65	2, 47	cofonr 8660	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠)
66		onss 7784	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
67	2, 66	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ On)
68	67	sselda 3943	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ On)
69	68	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝑞 ∈ On)
70		onss 7784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
71	70	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → 𝑦 ⊆ On)
72		sstr 3951	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑌 ⊆ 𝑦 ∧ 𝑦 ⊆ On) → 𝑌 ⊆ On)
73	72	expcom 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
74	71, 73	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
75	74	rexlimdva 3172	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
76	50, 75	mpd 16	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ⊆ On)
77	76	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → 𝑌 ⊆ On)
78	77	sselda 3943	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝑠 ∈ On)
79	1	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝐴 ∈ On)
80		naddss2 8677	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
81	69, 78, 79, 80	syl3anc 1396	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
82	81	rexbidva 3193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → (∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
83	82	ralbidva 3192	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠 ↔ ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
84	65, 83	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠))
85	1	snssd 4755	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴} ⊆ On)
86		xpss12 5677	. . . . . . . . . . . 12 ⊢ (({𝐴} ⊆ On ∧ 𝑌 ⊆ On) → ({𝐴} × 𝑌) ⊆ (On × On))
87	85, 76, 86	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴} × 𝑌) ⊆ (On × On))
88		sseq2 3969	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
89	88	imaeqexov 7649	. . . . . . . . . . 11 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
90	5, 87, 89	sylancr 598	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
91		oveq1 7418	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐴 → (𝑟 +no 𝑠) = (𝐴 +no 𝑠))
92	91	sseq2d 3975	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐴 → ((𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
93	92	rexbidv 3195	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐴 → (∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
94	93	rexsng 4645	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
95	1, 94	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
96	90, 95	bitrd 282	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
97	96	ralbidv 3194	. . . . . . . 8 ⊢ (𝜑 → (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
98	84, 97	mpbird 260	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑)
99		olc 881	. . . . . . . 8 ⊢ (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
100	99	ralimi 3108	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
101	98, 100	syl 18	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
102		rexun 4155	. . . . . . 7 ⊢ (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
103	102	ralbii 3117	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
104	101, 103	sylibr 237	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑)
105		xpss12 5677	. . . . . . . 8 ⊢ (({𝐴} ⊆ On ∧ 𝐵 ⊆ On) → ({𝐴} × 𝐵) ⊆ (On × On))
106	85, 67, 105	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ({𝐴} × 𝐵) ⊆ (On × On))
107		sseq1 3968	. . . . . . . . 9 ⊢ (𝑐 = (𝑝 +no 𝑞) → (𝑐 ⊆ 𝑑 ↔ (𝑝 +no 𝑞) ⊆ 𝑑))
108	107	rexbidv 3195	. . . . . . . 8 ⊢ (𝑐 = (𝑝 +no 𝑞) → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
109	108	imaeqalov 7650	. . . . . . 7 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
110	5, 106, 109	sylancr 598	. . . . . 6 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
111		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐴 → (𝑝 +no 𝑞) = (𝐴 +no 𝑞))
112	111	sseq1d 3974	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ 𝑑))
113	112	rexbidv 3195	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
114	113	ralbidv 3194	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
115	114	ralsng 4644	. . . . . . 7 ⊢ (𝐴 ∈ On → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
116	1, 115	syl 18	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
117	110, 116	bitrd 282	. . . . 5 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
118	104, 117	mpbird 260	. . . 4 ⊢ (𝜑 → ∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
119	1, 31	cofonr 8660	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟)
120		onss 7784	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
121	1, 120	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ On)
122	121	sselda 3943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ On)
123	122	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝑝 ∈ On)
124		ssintub 4933	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}
125	31, 121	eqsstrrd 3978	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ⊆ On)
126	124, 125	sstrid 3954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ On)
127	126	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑋 ⊆ On)
128	127	sselda 3943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝑟 ∈ On)
129	2	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝐵 ∈ On)
130		naddss1 8676	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ On ∧ 𝑟 ∈ On ∧ 𝐵 ∈ On) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
131	123, 128, 129, 130	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
132	131	rexbidva 3193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟 ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
133	132	ralbidva 3192	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟 ↔ ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
134	119, 133	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
135	2	snssd 4755	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ⊆ On)
136		xpss12 5677	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ On ∧ {𝐵} ⊆ On) → (𝑋 × {𝐵}) ⊆ (On × On))
137	126, 135, 136	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 × {𝐵}) ⊆ (On × On))
138		sseq2 3969	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
139	138	imaeqexov 7649	. . . . . . . . . . . 12 ⊢ (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
140	5, 137, 139	sylancr 598	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
141		oveq2 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝐵 → (𝑟 +no 𝑠) = (𝑟 +no 𝐵))
142	141	sseq2d 3975	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐵 → ((𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
143	142	rexsng 4645	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
144	2, 143	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
145	144	rexbidv 3195	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
146	140, 145	bitrd 282	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
147	146	ralbidv 3194	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
148	134, 147	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑)
149		orc 880	. . . . . . . . 9 ⊢ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
150	149	ralimi 3108	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
151	148, 150	syl 18	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
152		rexun 4155	. . . . . . . 8 ⊢ (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
153	152	ralbii 3117	. . . . . . 7 ⊢ (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
154	151, 153	sylibr 237	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑)
155		oveq2 7419	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐵 → (𝑝 +no 𝑞) = (𝑝 +no 𝐵))
156	155	sseq1d 3974	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ 𝑑))
157	156	rexbidv 3195	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
158	157	ralsng 4644	. . . . . . . 8 ⊢ (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
159	2, 158	syl 18	. . . . . . 7 ⊢ (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
160	159	ralbidv 3194	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
161	154, 160	mpbird 260	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑)
162		xpss12 5677	. . . . . . 7 ⊢ ((𝐴 ⊆ On ∧ {𝐵} ⊆ On) → (𝐴 × {𝐵}) ⊆ (On × On))
163	121, 135, 162	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝐵}) ⊆ (On × On))
164	108	imaeqalov 7650	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
165	5, 163, 164	sylancr 598	. . . . 5 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
166	161, 165	mpbird 260	. . . 4 ⊢ (𝜑 → ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
167		ralunb 4156	. . . 4 ⊢ (∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ∧ ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑))
168	118, 166, 167	sylanbrc 594	. . 3 ⊢ (𝜑 → ∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
169	124, 31	sseqtrrid 3986	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
170	169	sselda 3943	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝐴)
171		ssid 3965	. . . . . . . . . . 11 ⊢ 𝑝 ⊆ 𝑝
172		sseq2 3969	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑝 → (𝑝 ⊆ 𝑟 ↔ 𝑝 ⊆ 𝑝))
173	172	rspcev 3588	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝 ⊆ 𝑝) → ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
174	170, 171, 173	sylancl 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
175	174	ralrimiva 3163	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
176	126	sselda 3943	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ On)
177	176	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝑝 ∈ On)
178	121	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝐴 ⊆ On)
179	178	sselda 3943	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ On)
180	2	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝐵 ∈ On)
181	177, 179, 180, 130	syl3anc 1396	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
182	181	rexbidva 3193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟 ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
183	182	ralbidva 3192	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟 ↔ ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
184	175, 183	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
185		sseq2 3969	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
186	185	imaeqexov 7649	. . . . . . . . . . 11 ⊢ (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
187	5, 163, 186	sylancr 598	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
188	144	rexbidv 3195	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
189	187, 188	bitrd 282	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
190	189	ralbidv 3194	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
191	184, 190	mpbird 260	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)
192		olc 881	. . . . . . . 8 ⊢ (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
193	192	ralimi 3108	. . . . . . 7 ⊢ (∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
194	191, 193	syl 18	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
195	155	sseq1d 3974	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ 𝑏))
196	195	rexbidv 3195	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐵 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
197	196	ralsng 4644	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
198	2, 197	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
199	198	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
200		rexun 4155	. . . . . . . 8 ⊢ (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
201	199, 200	bitrdi 290	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
202	201	ralbidva 3192	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
203	194, 202	mpbird 260	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
204		sseq1 3968	. . . . . . . 8 ⊢ (𝑎 = (𝑝 +no 𝑞) → (𝑎 ⊆ 𝑏 ↔ (𝑝 +no 𝑞) ⊆ 𝑏))
205	204	rexbidv 3195	. . . . . . 7 ⊢ (𝑎 = (𝑝 +no 𝑞) → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
206	205	imaeqalov 7650	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
207	5, 137, 206	sylancr 598	. . . . 5 ⊢ (𝜑 → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
208	203, 207	mpbird 260	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
209		ssintub 4933	. . . . . . . . . . . . 13 ⊢ 𝑌 ⊆ ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦}
210	209, 47	sseqtrrid 3986	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ⊆ 𝐵)
211	210	sselda 3943	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝑞 ∈ 𝐵)
212		ssid 3965	. . . . . . . . . . 11 ⊢ 𝑞 ⊆ 𝑞
213		sseq2 3969	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑞 → (𝑞 ⊆ 𝑠 ↔ 𝑞 ⊆ 𝑞))
214	213	rspcev 3588	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ 𝐵 ∧ 𝑞 ⊆ 𝑞) → ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
215	211, 212, 214	sylancl 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
216	215	ralrimiva 3163	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
217	92	rexbidv 3195	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐴 → (∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
218	217	rexsng 4645	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
219	1, 218	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
220	219	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
221		sseq2 3969	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
222	221	imaeqexov 7649	. . . . . . . . . . . . 13 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
223	5, 106, 222	sylancr 598	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
224	223	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
225	76	sselda 3943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝑞 ∈ On)
226	225	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑞 ∈ On)
227	67	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝐵 ⊆ On)
228	227	sselda 3943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ On)
229	1	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝐴 ∈ On)
230	226, 228, 229, 80	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
231	230	rexbidva 3193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
232	220, 224, 231	3bitr4d 314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠))
233	232	ralbidva 3192	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠))
234	216, 233	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏)
235		orc 880	. . . . . . . . 9 ⊢ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
236	235	ralimi 3108	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
237	234, 236	syl 18	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
238		rexun 4155	. . . . . . . 8 ⊢ (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
239	238	ralbii 3117	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
240	237, 239	sylibr 237	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏)
241	111	sseq1d 3974	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ 𝑏))
242	241	rexbidv 3195	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
243	242	ralbidv 3194	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
244	243	ralsng 4644	. . . . . . 7 ⊢ (𝐴 ∈ On → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
245	1, 244	syl 18	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
246	240, 245	mpbird 260	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
247	205	imaeqalov 7650	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
248	5, 87, 247	sylancr 598	. . . . 5 ⊢ (𝜑 → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
249	246, 248	mpbird 260	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
250		ralunb 4156	. . . 4 ⊢ (∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ∧ ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏))
251	208, 249, 250	sylanbrc 594	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
252	30, 64, 168, 251	cofon2 8659	. 2 ⊢ (𝜑 → ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤} = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
253	4, 252	eqtrd 2804	1 ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  {crab 3422  Vcvv 3461   ∪ cun 3909   ⊆ wss 3911  𝒫 cpw 4565  {csn 4592  ∩ cint 4914   × cxp 5660  ran crn 5663   “ cima 5665  Oncon0 6361  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  (class class class)co 7411   +no cnadd 8651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-frecs 8278  df-nadd 8652

This theorem is referenced by:  naddasslem1  8681  naddasslem2  8682