Theorem naddunif 8660

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 8647	. . 3 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
4	1, 2, 3	syl2anc 584	. 2 ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤})
5		naddfn 8642	. . . . . . 7 ⊢ +no Fn (On × On)
6		fnfun 6621	. . . . . . 7 ⊢ ( +no Fn (On × On) → Fun +no )
7	5, 6	ax-mp 5	. . . . . 6 ⊢ Fun +no
8		snex 5394	. . . . . . 7 ⊢ {𝐴} ∈ V
9		xpexg 7729	. . . . . . 7 ⊢ (({𝐴} ∈ V ∧ 𝐵 ∈ On) → ({𝐴} × 𝐵) ∈ V)
10	8, 2, 9	sylancr 587	. . . . . 6 ⊢ (𝜑 → ({𝐴} × 𝐵) ∈ V)
11		funimaexg 6606	. . . . . 6 ⊢ ((Fun +no ∧ ({𝐴} × 𝐵) ∈ V) → ( +no “ ({𝐴} × 𝐵)) ∈ V)
12	7, 10, 11	sylancr 587	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ V)
13		imassrn 6045	. . . . . . 7 ⊢ ( +no “ ({𝐴} × 𝐵)) ⊆ ran +no
14		naddf 8648	. . . . . . . 8 ⊢ +no :(On × On)⟶On
15		frn 6698	. . . . . . . 8 ⊢ ( +no :(On × On)⟶On → ran +no ⊆ On)
16	14, 15	ax-mp 5	. . . . . . 7 ⊢ ran +no ⊆ On
17	13, 16	sstri 3959	. . . . . 6 ⊢ ( +no “ ({𝐴} × 𝐵)) ⊆ On
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ⊆ On)
19	12, 18	elpwd 4572	. . . 4 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On)
20		snex 5394	. . . . . . 7 ⊢ {𝐵} ∈ V
21		xpexg 7729	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ {𝐵} ∈ V) → (𝐴 × {𝐵}) ∈ V)
22	1, 20, 21	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ V)
23		funimaexg 6606	. . . . . 6 ⊢ ((Fun +no ∧ (𝐴 × {𝐵}) ∈ V) → ( +no “ (𝐴 × {𝐵})) ∈ V)
24	7, 22, 23	sylancr 587	. . . . 5 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ V)
25		imassrn 6045	. . . . . . 7 ⊢ ( +no “ (𝐴 × {𝐵})) ⊆ ran +no
26	25, 16	sstri 3959	. . . . . 6 ⊢ ( +no “ (𝐴 × {𝐵})) ⊆ On
27	26	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ⊆ On)
28	24, 27	elpwd 4572	. . . 4 ⊢ (𝜑 → ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On)
29		pwuncl 7749	. . . 4 ⊢ ((( +no “ ({𝐴} × 𝐵)) ∈ 𝒫 On ∧ ( +no “ (𝐴 × {𝐵})) ∈ 𝒫 On) → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
30	19, 28, 29	syl2anc 584	. . 3 ⊢ (𝜑 → (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ∈ 𝒫 On)
31		naddunif.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})
32	31, 1	eqeltrrd 2830	. . . . . . . . 9 ⊢ (𝜑 → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ∈ On)
33		onintrab2 7776	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 ↔ ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ∈ On)
34	32, 33	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ On 𝑋 ⊆ 𝑥)
35		vex 3454	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
36	35	ssex 5279	. . . . . . . . 9 ⊢ (𝑋 ⊆ 𝑥 → 𝑋 ∈ V)
37	36	rexlimivw 3131	. . . . . . . 8 ⊢ (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 → 𝑋 ∈ V)
38	34, 37	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ V)
39		xpexg 7729	. . . . . . 7 ⊢ ((𝑋 ∈ V ∧ {𝐵} ∈ V) → (𝑋 × {𝐵}) ∈ V)
40	38, 20, 39	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑋 × {𝐵}) ∈ V)
41		funimaexg 6606	. . . . . 6 ⊢ ((Fun +no ∧ (𝑋 × {𝐵}) ∈ V) → ( +no “ (𝑋 × {𝐵})) ∈ V)
42	7, 40, 41	sylancr 587	. . . . 5 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ V)
43		imassrn 6045	. . . . . . 7 ⊢ ( +no “ (𝑋 × {𝐵})) ⊆ ran +no
44	43, 16	sstri 3959	. . . . . 6 ⊢ ( +no “ (𝑋 × {𝐵})) ⊆ On
45	44	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ⊆ On)
46	42, 45	elpwd 4572	. . . 4 ⊢ (𝜑 → ( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On)
47		naddunif.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦})
48	47, 2	eqeltrrd 2830	. . . . . . . . 9 ⊢ (𝜑 → ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦} ∈ On)
49		onintrab2 7776	. . . . . . . . 9 ⊢ (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 ↔ ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦} ∈ On)
50	48, 49	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → ∃𝑦 ∈ On 𝑌 ⊆ 𝑦)
51		vex 3454	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
52	51	ssex 5279	. . . . . . . . 9 ⊢ (𝑌 ⊆ 𝑦 → 𝑌 ∈ V)
53	52	rexlimivw 3131	. . . . . . . 8 ⊢ (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 → 𝑌 ∈ V)
54	50, 53	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ V)
55		xpexg 7729	. . . . . . 7 ⊢ (({𝐴} ∈ V ∧ 𝑌 ∈ V) → ({𝐴} × 𝑌) ∈ V)
56	8, 54, 55	sylancr 587	. . . . . 6 ⊢ (𝜑 → ({𝐴} × 𝑌) ∈ V)
57		funimaexg 6606	. . . . . 6 ⊢ ((Fun +no ∧ ({𝐴} × 𝑌) ∈ V) → ( +no “ ({𝐴} × 𝑌)) ∈ V)
58	7, 56, 57	sylancr 587	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ V)
59		imassrn 6045	. . . . . . 7 ⊢ ( +no “ ({𝐴} × 𝑌)) ⊆ ran +no
60	59, 16	sstri 3959	. . . . . 6 ⊢ ( +no “ ({𝐴} × 𝑌)) ⊆ On
61	60	a1i 11	. . . . 5 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ⊆ On)
62	58, 61	elpwd 4572	. . . 4 ⊢ (𝜑 → ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On)
63		pwuncl 7749	. . . 4 ⊢ ((( +no “ (𝑋 × {𝐵})) ∈ 𝒫 On ∧ ( +no “ ({𝐴} × 𝑌)) ∈ 𝒫 On) → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
64	46, 62, 63	syl2anc 584	. . 3 ⊢ (𝜑 → (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ∈ 𝒫 On)
65	2, 47	cofonr 8641	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠)
66		onss 7764	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
67	2, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ On)
68	67	sselda 3949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ On)
69	68	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝑞 ∈ On)
70		onss 7764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
71	70	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → 𝑦 ⊆ On)
72		sstr 3958	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑌 ⊆ 𝑦 ∧ 𝑦 ⊆ On) → 𝑌 ⊆ On)
73	72	expcom 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ On → (𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
74	71, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
75	74	rexlimdva 3135	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∃𝑦 ∈ On 𝑌 ⊆ 𝑦 → 𝑌 ⊆ On))
76	50, 75	mpd 15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ⊆ On)
77	76	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → 𝑌 ⊆ On)
78	77	sselda 3949	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝑠 ∈ On)
79	1	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → 𝐴 ∈ On)
80		naddss2 8657	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ On ∧ 𝑠 ∈ On ∧ 𝐴 ∈ On) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
81	69, 78, 79, 80	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝐵) ∧ 𝑠 ∈ 𝑌) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
82	81	rexbidva 3156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐵) → (∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
83	82	ralbidva 3155	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 𝑞 ⊆ 𝑠 ↔ ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
84	65, 83	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠))
85	1	snssd 4776	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴} ⊆ On)
86		xpss12 5656	. . . . . . . . . . . 12 ⊢ (({𝐴} ⊆ On ∧ 𝑌 ⊆ On) → ({𝐴} × 𝑌) ⊆ (On × On))
87	85, 76, 86	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴} × 𝑌) ⊆ (On × On))
88		sseq2 3976	. . . . . . . . . . . 12 ⊢ (𝑑 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
89	88	imaeqexov 7630	. . . . . . . . . . 11 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
90	5, 87, 89	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
91		oveq1 7397	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐴 → (𝑟 +no 𝑠) = (𝐴 +no 𝑠))
92	91	sseq2d 3982	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝐴 → ((𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
93	92	rexbidv 3158	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝐴 → (∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
94	93	rexsng 4643	. . . . . . . . . . 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 3157	. . . . . . . 8 ⊢ (𝜑 → (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝑌 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
98	84, 97	mpbird 257	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑)
99		olc 868	. . . . . . . 8 ⊢ (∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
100	99	ralimi 3067	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑 → ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
101	98, 100	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
102		rexun 4162	. . . . . . 7 ⊢ (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
103	102	ralbii 3076	. . . . . 6 ⊢ (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝐴 +no 𝑞) ⊆ 𝑑))
104	101, 103	sylibr 234	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑)
105		xpss12 5656	. . . . . . . 8 ⊢ (({𝐴} ⊆ On ∧ 𝐵 ⊆ On) → ({𝐴} × 𝐵) ⊆ (On × On))
106	85, 67, 105	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ({𝐴} × 𝐵) ⊆ (On × On))
107		sseq1 3975	. . . . . . . . 9 ⊢ (𝑐 = (𝑝 +no 𝑞) → (𝑐 ⊆ 𝑑 ↔ (𝑝 +no 𝑞) ⊆ 𝑑))
108	107	rexbidv 3158	. . . . . . . 8 ⊢ (𝑐 = (𝑝 +no 𝑞) → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
109	108	imaeqalov 7631	. . . . . . 7 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
110	5, 106, 109	sylancr 587	. . . . . 6 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
111		oveq1 7397	. . . . . . . . . . 11 ⊢ (𝑝 = 𝐴 → (𝑝 +no 𝑞) = (𝐴 +no 𝑞))
112	111	sseq1d 3981	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝐴 +no 𝑞) ⊆ 𝑑))
113	112	rexbidv 3158	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
114	113	ralbidv 3157	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑞 ∈ 𝐵 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝐴 +no 𝑞) ⊆ 𝑑))
115	114	ralsng 4642	. . . . . . 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 8641	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟)
120		onss 7764	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
121	1, 120	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ On)
122	121	sselda 3949	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ On)
123	122	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝑝 ∈ On)
124		ssintub 4933	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}
125	31, 121	eqsstrrd 3985	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ⊆ On)
126	124, 125	sstrid 3961	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ On)
127	126	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑋 ⊆ On)
128	127	sselda 3949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝑟 ∈ On)
129	2	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → 𝐵 ∈ On)
130		naddss1 8656	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ On ∧ 𝑟 ∈ On ∧ 𝐵 ∈ On) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
131	123, 128, 129, 130	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝐴) ∧ 𝑟 ∈ 𝑋) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
132	131	rexbidva 3156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟 ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
133	132	ralbidva 3155	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 𝑝 ⊆ 𝑟 ↔ ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
134	119, 133	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
135	2	snssd 4776	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ⊆ On)
136		xpss12 5656	. . . . . . . . . . . . 13 ⊢ ((𝑋 ⊆ On ∧ {𝐵} ⊆ On) → (𝑋 × {𝐵}) ⊆ (On × On))
137	126, 135, 136	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 × {𝐵}) ⊆ (On × On))
138		sseq2 3976	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
139	138	imaeqexov 7630	. . . . . . . . . . . 12 ⊢ (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
140	5, 137, 139	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
141		oveq2 7398	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝐵 → (𝑟 +no 𝑠) = (𝑟 +no 𝐵))
142	141	sseq2d 3982	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝐵 → ((𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
143	142	rexsng 4643	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
144	2, 143	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
145	144	rexbidv 3158	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
146	140, 145	bitrd 279	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
147	146	ralbidv 3157	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝑋 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
148	134, 147	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑)
149		orc 867	. . . . . . . . 9 ⊢ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
150	149	ralimi 3067	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 → ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
151	148, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
152		rexun 4162	. . . . . . . 8 ⊢ (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
153	152	ralbii 3076	. . . . . . 7 ⊢ (∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 (∃𝑑 ∈ ( +no “ (𝑋 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑑 ∨ ∃𝑑 ∈ ( +no “ ({𝐴} × 𝑌))(𝑝 +no 𝐵) ⊆ 𝑑))
154	151, 153	sylibr 234	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑)
155		oveq2 7398	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐵 → (𝑝 +no 𝑞) = (𝑝 +no 𝐵))
156	155	sseq1d 3981	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑑 ↔ (𝑝 +no 𝐵) ⊆ 𝑑))
157	156	rexbidv 3158	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → (∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
158	157	ralsng 4642	. . . . . . . 8 ⊢ (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
159	2, 158	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
160	159	ralbidv 3157	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝐵) ⊆ 𝑑))
161	154, 160	mpbird 257	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑)
162		xpss12 5656	. . . . . . 7 ⊢ ((𝐴 ⊆ On ∧ {𝐵} ⊆ On) → (𝐴 × {𝐵}) ⊆ (On × On))
163	121, 135, 162	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝐵}) ⊆ (On × On))
164	108	imaeqalov 7631	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
165	5, 163, 164	sylancr 587	. . . . 5 ⊢ (𝜑 → (∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝐵}∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))(𝑝 +no 𝑞) ⊆ 𝑑))
166	161, 165	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
167		ralunb 4163	. . . 4 ⊢ (∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ↔ (∀𝑐 ∈ ( +no “ ({𝐴} × 𝐵))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑 ∧ ∀𝑐 ∈ ( +no “ (𝐴 × {𝐵}))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑))
168	118, 166, 167	sylanbrc 583	. . 3 ⊢ (𝜑 → ∀𝑐 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))∃𝑑 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))𝑐 ⊆ 𝑑)
169	124, 31	sseqtrrid 3993	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
170	169	sselda 3949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝐴)
171		ssid 3972	. . . . . . . . . . 11 ⊢ 𝑝 ⊆ 𝑝
172		sseq2 3976	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑝 → (𝑝 ⊆ 𝑟 ↔ 𝑝 ⊆ 𝑝))
173	172	rspcev 3591	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ 𝐴 ∧ 𝑝 ⊆ 𝑝) → ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
174	170, 171, 173	sylancl 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
175	174	ralrimiva 3126	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟)
176	126	sselda 3949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ On)
177	176	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝑝 ∈ On)
178	121	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝐴 ⊆ On)
179	178	sselda 3949	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ On)
180	2	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → 𝐵 ∈ On)
181	177, 179, 180, 130	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑟 ∈ 𝐴) → (𝑝 ⊆ 𝑟 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
182	181	rexbidva 3156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟 ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
183	182	ralbidva 3155	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 𝑝 ⊆ 𝑟 ↔ ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
184	175, 183	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵))
185		sseq2 3976	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑟 +no 𝑠) → ((𝑝 +no 𝐵) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
186	185	imaeqexov 7630	. . . . . . . . . . 11 ⊢ (( +no Fn (On × On) ∧ (𝐴 × {𝐵}) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
187	5, 163, 186	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠)))
188	144	rexbidv 3158	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ {𝐵} (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
189	187, 188	bitrd 279	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
190	189	ralbidv 3157	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∃𝑟 ∈ 𝐴 (𝑝 +no 𝐵) ⊆ (𝑟 +no 𝐵)))
191	184, 190	mpbird 257	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)
192		olc 868	. . . . . . . 8 ⊢ (∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
193	192	ralimi 3067	. . . . . . 7 ⊢ (∀𝑝 ∈ 𝑋 ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏 → ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
194	191, 193	syl 17	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
195	155	sseq1d 3981	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝐵 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝑝 +no 𝐵) ⊆ 𝑏))
196	195	rexbidv 3158	. . . . . . . . . . 11 ⊢ (𝑞 = 𝐵 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
197	196	ralsng 4642	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
198	2, 197	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
199	198	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏))
200		rexun 4162	. . . . . . . 8 ⊢ (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝐵) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏))
201	199, 200	bitrdi 287	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
202	201	ralbidva 3155	. . . . . 6 ⊢ (𝜑 → (∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝑝 +no 𝐵) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝑝 +no 𝐵) ⊆ 𝑏)))
203	194, 202	mpbird 257	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏)
204		sseq1 3975	. . . . . . . 8 ⊢ (𝑎 = (𝑝 +no 𝑞) → (𝑎 ⊆ 𝑏 ↔ (𝑝 +no 𝑞) ⊆ 𝑏))
205	204	rexbidv 3158	. . . . . . 7 ⊢ (𝑎 = (𝑝 +no 𝑞) → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
206	205	imaeqalov 7631	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ (𝑋 × {𝐵}) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
207	5, 137, 206	sylancr 587	. . . . 5 ⊢ (𝜑 → (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ {𝐵}∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
208	203, 207	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
209		ssintub 4933	. . . . . . . . . . . . 13 ⊢ 𝑌 ⊆ ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦}
210	209, 47	sseqtrrid 3993	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ⊆ 𝐵)
211	210	sselda 3949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝑞 ∈ 𝐵)
212		ssid 3972	. . . . . . . . . . 11 ⊢ 𝑞 ⊆ 𝑞
213		sseq2 3976	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑞 → (𝑞 ⊆ 𝑠 ↔ 𝑞 ⊆ 𝑞))
214	213	rspcev 3591	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ 𝐵 ∧ 𝑞 ⊆ 𝑞) → ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
215	211, 212, 214	sylancl 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
216	215	ralrimiva 3126	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠)
217	92	rexbidv 3158	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝐴 → (∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
218	217	rexsng 4643	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ On → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
219	1, 218	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
220	219	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠) ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
221		sseq2 3976	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑟 +no 𝑠) → ((𝐴 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
222	221	imaeqexov 7630	. . . . . . . . . . . . 13 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝐵) ⊆ (On × On)) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
223	5, 106, 222	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
224	223	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑟 ∈ {𝐴}∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝑟 +no 𝑠)))
225	76	sselda 3949	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝑞 ∈ On)
226	225	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑞 ∈ On)
227	67	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → 𝐵 ⊆ On)
228	227	sselda 3949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ On)
229	1	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → 𝐴 ∈ On)
230	226, 228, 229, 80	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑌) ∧ 𝑠 ∈ 𝐵) → (𝑞 ⊆ 𝑠 ↔ (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
231	230	rexbidva 3156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝐵 (𝐴 +no 𝑞) ⊆ (𝐴 +no 𝑠)))
232	220, 224, 231	3bitr4d 311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑌) → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠))
233	232	ralbidva 3155	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑠 ∈ 𝐵 𝑞 ⊆ 𝑠))
234	216, 233	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏)
235		orc 867	. . . . . . . . 9 ⊢ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
236	235	ralimi 3067	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 → ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
237	234, 236	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
238		rexun 4162	. . . . . . . 8 ⊢ (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
239	238	ralbii 3076	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 (∃𝑏 ∈ ( +no “ ({𝐴} × 𝐵))(𝐴 +no 𝑞) ⊆ 𝑏 ∨ ∃𝑏 ∈ ( +no “ (𝐴 × {𝐵}))(𝐴 +no 𝑞) ⊆ 𝑏))
240	237, 239	sylibr 234	. . . . . 6 ⊢ (𝜑 → ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏)
241	111	sseq1d 3981	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → ((𝑝 +no 𝑞) ⊆ 𝑏 ↔ (𝐴 +no 𝑞) ⊆ 𝑏))
242	241	rexbidv 3158	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → (∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
243	242	ralbidv 3157	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏 ↔ ∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝐴 +no 𝑞) ⊆ 𝑏))
244	243	ralsng 4642	. . . . . . 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 7631	. . . . . 6 ⊢ (( +no Fn (On × On) ∧ ({𝐴} × 𝑌) ⊆ (On × On)) → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
248	5, 87, 247	sylancr 587	. . . . 5 ⊢ (𝜑 → (∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ ∀𝑝 ∈ {𝐴}∀𝑞 ∈ 𝑌 ∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))(𝑝 +no 𝑞) ⊆ 𝑏))
249	246, 248	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
250		ralunb 4163	. . . 4 ⊢ (∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ↔ (∀𝑎 ∈ ( +no “ (𝑋 × {𝐵}))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏 ∧ ∀𝑎 ∈ ( +no “ ({𝐴} × 𝑌))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏))
251	208, 249, 250	sylanbrc 583	. . 3 ⊢ (𝜑 → ∀𝑎 ∈ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌)))∃𝑏 ∈ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵})))𝑎 ⊆ 𝑏)
252	30, 64, 168, 251	cofon2 8640	. 2 ⊢ (𝜑 → ∩ {𝑤 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑤} = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
253	4, 252	eqtrd 2765	1 ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  {crab 3408  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  𝒫 cpw 4566  {csn 4592  ∩ cint 4913   × cxp 5639  ran crn 5642   “ cima 5644  Oncon0 6335  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510  (class class class)co 7390   +no cnadd 8632

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-frecs 8263  df-nadd 8633

This theorem is referenced by:  naddasslem1  8661  naddasslem2  8662