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 585	. 2 ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
5		naddfn 8662	. . . . . . 7 ⊢ +no Fn (On × On)
6		fnfun 6641	. . . . . . 7 ⊢ ( +no Fn (On × On) → Fun +no )
7	5, 6	ax-mp 5	. . . . . 6 ⊢ Fun +no
8		snex 5427	. . . . . . 7 ⊢ {𝐴} ∈ V
9		xpexg 7724	. . . . . . 7 ⊢ (({𝐴} ∈ V ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ∈ V)
10	8, 2, 9	sylancr 588	. . . . . 6 ⊢ (𝜑 → ({𝐴} × 𝐵) ∈ V)
11		funimaexg 6626	. . . . . 6 ⊢ ((Fun +no ∧ ({𝐴} × 𝐵) ∈ V) → ( +no “ ({𝐴} × 𝐵)) ∈ V)
12	7, 10, 11	sylancr 588	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ V)
13		imassrn 6063	. . . . . . 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 3989	. . . . . 6 ⊢ ( +no “ ({𝐴} × 𝐵)) ⊆ On
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ⊆ On)
19	12, 18	elpwd 4604	. . . 4 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On)
20		snex 5427	. . . . . . 7 ⊢ {𝐵} ∈ V
21		xpexg 7724	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ {𝐵} ∈ V) → (𝐴 × {𝐵}) ∈ V)
22	1, 20, 21	sylancl 587	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ V)
23		funimaexg 6626	. . . . . 6 ⊢ ((Fun +no ∧ (𝐴 × {𝐵}) ∈ V) → ( +no “ (𝐴 × {𝐵})) ∈ V)
24	7, 22, 23	sylancr 588	. . . . 5 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ V)
25		imassrn 6063	. . . . . . 7 ⊢ ( +no “ (𝐴 × {𝐵})) ⊆ ran +no
26	25, 16	sstri 3989	. . . . . 6 ⊢ ( +no “ (𝐴 × {𝐵})) ⊆ On
27	26	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ⊆ On)
28	24, 27	elpwd 4604	. . . 4 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On)
29		pwuncl 7744	. . . 4 ⊢ ((( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On ∧ ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On) → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
30	19, 28, 29	syl2anc 585	. . 3 ⊢ (𝜑 → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
31		naddunif.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})
32	31, 1	eqeltrrd 2835	. . . . . . . . 9 ⊢ (𝜑 → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ∈ On)
33		onintrab2 7772	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 ↔ ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ∈ On)
34	32, 33	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ On 𝑋 ⊆ 𝑥)
35		vex 3479	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
36	35	ssex 5317	. . . . . . . . 9 ⊢ (𝑋 ⊆ 𝑥 → 𝑋 ∈ V)
37	36	rexlimivw 3152	. . . . . . . 8 ⊢ (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 → 𝑋 ∈ V)
38	34, 37	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ V)
39		xpexg 7724	. . . . . . 7 ⊢ ((𝑋 ∈ V ∧ {𝐵} ∈ V) → (𝑋 × {𝐵}) ∈ V)
40	38, 20, 39	sylancl 587	. . . . . 6 ⊢ (𝜑 → (𝑋 × {𝐵}) ∈ V)
41		funimaexg 6626	. . . . . 6 ⊢ ((Fun +no ∧ (𝑋 × {𝐵}) ∈ V) → ( +no “ (𝑋 × {𝐵})) ∈ V)
42	7, 40, 41	sylancr 588	. . . . 5 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ V)
43		imassrn 6063	. . . . . . 7 ⊢ ( +no “ (𝑋 × {𝐵})) ⊆ ran +no
44	43, 16	sstri 3989	. . . . . 6 ⊢ ( +no “ (𝑋 × {𝐵})) ⊆ On
45	44	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ⊆ On)
46	42, 45	elpwd 4604	. . . 4 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On)
47		naddunif.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦})
48	47, 2	eqeltrrd 2835	. . . . . . . . 9 ⊢ (𝜑 → ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦} ∈ On)
49		onintrab2 7772	. . . . . . . . 9 ⊢ (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 ↔ ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦} ∈ On)
50	48, 49	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → ∃𝑦 ∈ On 𝑌 ⊆ 𝑦)
51		vex 3479	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
52	51	ssex 5317	. . . . . . . . 9 ⊢ (𝑌 ⊆ 𝑦 → 𝑌 ∈ V)
53	52	rexlimivw 3152	. . . . . . . 8 ⊢ (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 → 𝑌 ∈ V)
54	50, 53	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ V)
55		xpexg 7724	. . . . . . 7 ⊢ (({𝐴} ∈ V ∧ 𝑌 ∈ V) → ({𝐴} × 𝑌) ∈ V)
56	8, 54, 55	sylancr 588	. . . . . 6 ⊢ (𝜑 → ({𝐴} × 𝑌) ∈ V)
57		funimaexg 6626	. . . . . 6 ⊢ ((Fun +no ∧ ({𝐴} × 𝑌) ∈ V) → ( +no “ ({𝐴} × 𝑌)) ∈ V)
58	7, 56, 57	sylancr 588	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ V)
59		imassrn 6063	. . . . . . 7 ⊢ ( +no “ ({𝐴} × 𝑌)) ⊆ ran +no
60	59, 16	sstri 3989	. . . . . 6 ⊢ ( +no “ ({𝐴} × 𝑌)) ⊆ On
61	60	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ⊆ On)
62	58, 61	elpwd 4604	. . . 4 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On)
63		pwuncl 7744	. . . 4 ⊢ ((( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On ∧ ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On) → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
64	46, 62, 63	syl2anc 585	. . 3 ⊢ (𝜑 → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
65	2, 47	cofonr 8661	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠)
66		onss 7759	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
67	2, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ On)
68	67	sselda 3980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ On)
69	68	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝑞 ∈ On)
70		onss 7759	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
71	70	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → 𝑦 ⊆ On)
72		sstr 3988	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑌 ⊆ 𝑦 ∧ 𝑦 ⊆ On) → 𝑌 ⊆ On)
73	72	expcom 415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
74	71, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
75	74	rexlimdva 3156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
76	50, 75	mpd 15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ⊆ On)
77	76	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → 𝑌 ⊆ On)
78	77	sselda 3980	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝑠 ∈ On)
79	1	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝐴 ∈ On)
80		naddss2 8677	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
81	69, 78, 79, 80	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
82	81	rexbidva 3177	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → (∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
83	82	ralbidva 3176	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠 ↔ ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
84	65, 83	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠))
85	1	snssd 4808	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴} ⊆ On)
86		xpss12 5687	. . . . . . . . . . . 12 ⊢ (({𝐴} ⊆ On ∧ 𝑌 ⊆ On) → ({𝐴} × 𝑌) ⊆ (On × On))
87	85, 76, 86	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴} × 𝑌) ⊆ (On × On))
88		sseq2 4006	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
89	88	imaeqexov 7632	. . . . . . . . . . 11 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
90	5, 87, 89	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
91		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐴 → (𝑟 +no 𝑠) = (𝐴 +no 𝑠))
92	91	sseq2d 4012	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐴 → ((𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
93	92	rexbidv 3179	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐴 → (∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
94	93	rexsng 4674	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
95	1, 94	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
96	90, 95	bitrd 279	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
97	96	ralbidv 3178	. . . . . . . 8 ⊢ (𝜑 → (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
98	84, 97	mpbird 257	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑)
99		olc 867	. . . . . . . 8 ⊢ (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
100	99	ralimi 3084	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
101	98, 100	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
102		rexun 4188	. . . . . . 7 ⊢ (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
103	102	ralbii 3094	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
104	101, 103	sylibr 233	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑)
105		xpss12 5687	. . . . . . . 8 ⊢ (({𝐴} ⊆ On ∧ 𝐵 ⊆ On) → ({𝐴} × 𝐵) ⊆ (On × On))
106	85, 67, 105	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ({𝐴} × 𝐵) ⊆ (On × On))
107		sseq1 4005	. . . . . . . . 9 ⊢ (𝑐 = (𝑝 +no 𝑞) → (𝑐 ⊆ 𝑑 ↔ (𝑝 +no 𝑞) ⊆ 𝑑))
108	107	rexbidv 3179	. . . . . . . 8 ⊢ (𝑐 = (𝑝 +no 𝑞) → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
109	108	imaeqalov 7633	. . . . . . 7 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
110	5, 106, 109	sylancr 588	. . . . . 6 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
111		oveq1 7403	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐴 → (𝑝 +no 𝑞) = (𝐴 +no 𝑞))
112	111	sseq1d 4011	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ 𝑑))
113	112	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
114	113	ralbidv 3178	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
115	114	ralsng 4673	. . . . . . 7 ⊢ (𝐴 ∈ On → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
116	1, 115	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
117	110, 116	bitrd 279	. . . . 5 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
118	104, 117	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
119	1, 31	cofonr 8661	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟)
120		onss 7759	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
121	1, 120	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ On)
122	121	sselda 3980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ On)
123	122	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝑝 ∈ On)
124		ssintub 4966	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}
125	31, 121	eqsstrrd 4019	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ⊆ On)
126	124, 125	sstrid 3991	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ On)
127	126	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑋 ⊆ On)
128	127	sselda 3980	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝑟 ∈ On)
129	2	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝐵 ∈ On)
130		naddss1 8676	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ On ∧ 𝑟 ∈ On ∧ 𝐵 ∈ On) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
131	123, 128, 129, 130	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
132	131	rexbidva 3177	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟 ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
133	132	ralbidva 3176	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟 ↔ ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
134	119, 133	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
135	2	snssd 4808	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ⊆ On)
136		xpss12 5687	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ On ∧ {𝐵} ⊆ On) → (𝑋 × {𝐵}) ⊆ (On × On))
137	126, 135, 136	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 × {𝐵}) ⊆ (On × On))
138		sseq2 4006	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
139	138	imaeqexov 7632	. . . . . . . . . . . 12 ⊢ (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
140	5, 137, 139	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
141		oveq2 7404	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝐵 → (𝑟 +no 𝑠) = (𝑟 +no 𝐵))
142	141	sseq2d 4012	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐵 → ((𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
143	142	rexsng 4674	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
144	2, 143	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
145	144	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
146	140, 145	bitrd 279	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
147	146	ralbidv 3178	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
148	134, 147	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑)
149		orc 866	. . . . . . . . 9 ⊢ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
150	149	ralimi 3084	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
151	148, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
152		rexun 4188	. . . . . . . 8 ⊢ (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
153	152	ralbii 3094	. . . . . . 7 ⊢ (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
154	151, 153	sylibr 233	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑)
155		oveq2 7404	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐵 → (𝑝 +no 𝑞) = (𝑝 +no 𝐵))
156	155	sseq1d 4011	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ 𝑑))
157	156	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
158	157	ralsng 4673	. . . . . . . 8 ⊢ (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
159	2, 158	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
160	159	ralbidv 3178	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
161	154, 160	mpbird 257	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑)
162		xpss12 5687	. . . . . . 7 ⊢ ((𝐴 ⊆ On ∧ {𝐵} ⊆ On) → (𝐴 × {𝐵}) ⊆ (On × On))
163	121, 135, 162	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝐵}) ⊆ (On × On))
164	108	imaeqalov 7633	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
165	5, 163, 164	sylancr 588	. . . . 5 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
166	161, 165	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
167		ralunb 4189	. . . 4 ⊢ (∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ∧ ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑))
168	118, 166, 167	sylanbrc 584	. . 3 ⊢ (𝜑 → ∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
169	124, 31	sseqtrrid 4033	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
170	169	sselda 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝐴)
171		ssid 4002	. . . . . . . . . . 11 ⊢ 𝑝 ⊆ 𝑝
172		sseq2 4006	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑝 → (𝑝 ⊆ 𝑟 ↔ 𝑝 ⊆ 𝑝))
173	172	rspcev 3611	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝 ⊆ 𝑝) → ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
174	170, 171, 173	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
175	174	ralrimiva 3147	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
176	126	sselda 3980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ On)
177	176	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝑝 ∈ On)
178	121	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝐴 ⊆ On)
179	178	sselda 3980	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ On)
180	2	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝐵 ∈ On)
181	177, 179, 180, 130	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
182	181	rexbidva 3177	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟 ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
183	182	ralbidva 3176	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟 ↔ ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
184	175, 183	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
185		sseq2 4006	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
186	185	imaeqexov 7632	. . . . . . . . . . 11 ⊢ (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
187	5, 163, 186	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
188	144	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
189	187, 188	bitrd 279	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
190	189	ralbidv 3178	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
191	184, 190	mpbird 257	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)
192		olc 867	. . . . . . . 8 ⊢ (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
193	192	ralimi 3084	. . . . . . 7 ⊢ (∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
194	191, 193	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
195	155	sseq1d 4011	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ 𝑏))
196	195	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐵 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
197	196	ralsng 4673	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
198	2, 197	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
199	198	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
200		rexun 4188	. . . . . . . 8 ⊢ (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
201	199, 200	bitrdi 287	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
202	201	ralbidva 3176	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
203	194, 202	mpbird 257	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
204		sseq1 4005	. . . . . . . 8 ⊢ (𝑎 = (𝑝 +no 𝑞) → (𝑎 ⊆ 𝑏 ↔ (𝑝 +no 𝑞) ⊆ 𝑏))
205	204	rexbidv 3179	. . . . . . 7 ⊢ (𝑎 = (𝑝 +no 𝑞) → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
206	205	imaeqalov 7633	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
207	5, 137, 206	sylancr 588	. . . . 5 ⊢ (𝜑 → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
208	203, 207	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
209		ssintub 4966	. . . . . . . . . . . . 13 ⊢ 𝑌 ⊆ ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦}
210	209, 47	sseqtrrid 4033	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ⊆ 𝐵)
211	210	sselda 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝑞 ∈ 𝐵)
212		ssid 4002	. . . . . . . . . . 11 ⊢ 𝑞 ⊆ 𝑞
213		sseq2 4006	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑞 → (𝑞 ⊆ 𝑠 ↔ 𝑞 ⊆ 𝑞))
214	213	rspcev 3611	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ 𝐵 ∧ 𝑞 ⊆ 𝑞) → ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
215	211, 212, 214	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
216	215	ralrimiva 3147	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
217	92	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐴 → (∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
218	217	rexsng 4674	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
219	1, 218	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
220	219	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
221		sseq2 4006	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
222	221	imaeqexov 7632	. . . . . . . . . . . . 13 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
223	5, 106, 222	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
224	223	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
225	76	sselda 3980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝑞 ∈ On)
226	225	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑞 ∈ On)
227	67	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝐵 ⊆ On)
228	227	sselda 3980	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ On)
229	1	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝐴 ∈ On)
230	226, 228, 229, 80	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
231	230	rexbidva 3177	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
232	220, 224, 231	3bitr4d 311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠))
233	232	ralbidva 3176	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠))
234	216, 233	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏)
235		orc 866	. . . . . . . . 9 ⊢ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
236	235	ralimi 3084	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
237	234, 236	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
238		rexun 4188	. . . . . . . 8 ⊢ (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
239	238	ralbii 3094	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
240	237, 239	sylibr 233	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏)
241	111	sseq1d 4011	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ 𝑏))
242	241	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
243	242	ralbidv 3178	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
244	243	ralsng 4673	. . . . . . 7 ⊢ (𝐴 ∈ On → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
245	1, 244	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
246	240, 245	mpbird 257	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
247	205	imaeqalov 7633	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
248	5, 87, 247	sylancr 588	. . . . 5 ⊢ (𝜑 → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
249	246, 248	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
250		ralunb 4189	. . . 4 ⊢ (∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ∧ ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏))
251	208, 249, 250	sylanbrc 584	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
252	30, 64, 168, 251	cofon2 8660	. 2 ⊢ (𝜑 → ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤} = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
253	4, 252	eqtrd 2773	1 ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  {crab 3433  Vcvv 3475   ∪ cun 3944   ⊆ wss 3946  𝒫 cpw 4598  {csn 4624  ∩ cint 4946   × cxp 5670  ran crn 5673   “ cima 5675  Oncon0 6356  Fun wfun 6529   Fn wfn 6530  ⟶wf 6531  (class class class)co 7396   +no cnadd 8652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7962  df-2nd 7963  df-frecs 8253  df-nadd 8653

This theorem is referenced by:  naddasslem1  8681  naddasslem2  8682