naddunif

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

	Ref	Expression
Hypotheses	naddunif.1	$⊢ φ \to A \in On$
	naddunif.2	$⊢ φ \to B \in On$
	naddunif.3	$⊢ φ \to A = ⋂ \{x \in On \| X \subseteq x\}$
	naddunif.4	$⊢ φ \to B = ⋂ \{y \in On \| Y \subseteq y\}$
Assertion	naddunif	$⊢ φ \to A + B = ⋂ \{z \in On \| + [X \times \{B\}] \cup + [\{A\} \times Y] \subseteq z\}$

Proof

Step	Hyp	Ref	Expression
1		naddunif.1	$⊢ φ \to A \in On$
2		naddunif.2	$⊢ φ \to B \in On$
3		naddunif.3	$⊢ φ \to A = ⋂ \{x \in On \| X \subseteq x\}$
4		naddunif.4	$⊢ φ \to B = ⋂ \{y \in On \| Y \subseteq y\}$
5		naddov3	$⊢ (A \in On \land B \in On) \to A + B = ⋂ \{w \in On \| + [\{A\} \times B] \cup + [A \times \{B\}] \subseteq w\}$
6	1 2 5	syl2anc	$⊢ φ \to A + B = ⋂ \{w \in On \| + [\{A\} \times B] \cup + [A \times \{B\}] \subseteq w\}$
7		naddfn	$⊢ + Fn (On \times On)$
8		fnfun	$⊢ + Fn (On \times On) \to Fun +$
9	7 8	ax-mp	$⊢ Fun +$
10		snex	$⊢ \{A\} \in V$
11		xpexg	$⊢ (\{A\} \in V \land B \in On) \to \{A\} \times B \in V$
12	10 2 11	sylancr	$⊢ φ \to \{A\} \times B \in V$
13		funimaexg	$⊢ (Fun + \land \{A\} \times B \in V) \to + [\{A\} \times B] \in V$
14	9 12 13	sylancr	$⊢ φ \to + [\{A\} \times B] \in V$
15		imassrn	$⊢ + [\{A\} \times B] \subseteq ran +$
16		naddf	$⊢ + : On \times On ⟶ On$
17		frn	$⊢ + : On \times On ⟶ On \to ran + \subseteq On$
18	16 17	ax-mp	$⊢ ran + \subseteq On$
19	15 18	sstri	$⊢ + [\{A\} \times B] \subseteq On$
20	19	a1i	$⊢ φ \to + [\{A\} \times B] \subseteq On$
21	14 20	elpwd	$⊢ φ \to + [\{A\} \times B] \in 𝒫 On$
22		snex	$⊢ \{B\} \in V$
23		xpexg	$⊢ (A \in On \land \{B\} \in V) \to A \times \{B\} \in V$
24	1 22 23	sylancl	$⊢ φ \to A \times \{B\} \in V$
25		funimaexg	$⊢ (Fun + \land A \times \{B\} \in V) \to + [A \times \{B\}] \in V$
26	9 24 25	sylancr	$⊢ φ \to + [A \times \{B\}] \in V$
27		imassrn	$⊢ + [A \times \{B\}] \subseteq ran +$
28	27 18	sstri	$⊢ + [A \times \{B\}] \subseteq On$
29	28	a1i	$⊢ φ \to + [A \times \{B\}] \subseteq On$
30	26 29	elpwd	$⊢ φ \to + [A \times \{B\}] \in 𝒫 On$
31		pwuncl	$⊢ (+ [\{A\} \times B] \in 𝒫 On \land + [A \times \{B\}] \in 𝒫 On) \to + [\{A\} \times B] \cup + [A \times \{B\}] \in 𝒫 On$
32	21 30 31	syl2anc	$⊢ φ \to + [\{A\} \times B] \cup + [A \times \{B\}] \in 𝒫 On$
33	3 1	eqeltrrd	$⊢ φ \to ⋂ \{x \in On \| X \subseteq x\} \in On$
34		onintrab2	$⊢ \exists x \in On X \subseteq x \leftrightarrow ⋂ \{x \in On \| X \subseteq x\} \in On$
35	33 34	sylibr	$⊢ φ \to \exists x \in On X \subseteq x$
36		vex	$⊢ x \in V$
37	36	ssex	$⊢ X \subseteq x \to X \in V$
38	37	rexlimivw	$⊢ \exists x \in On X \subseteq x \to X \in V$
39	35 38	syl	$⊢ φ \to X \in V$
40		xpexg	$⊢ (X \in V \land \{B\} \in V) \to X \times \{B\} \in V$
41	39 22 40	sylancl	$⊢ φ \to X \times \{B\} \in V$
42		funimaexg	$⊢ (Fun + \land X \times \{B\} \in V) \to + [X \times \{B\}] \in V$
43	9 41 42	sylancr	$⊢ φ \to + [X \times \{B\}] \in V$
44		imassrn	$⊢ + [X \times \{B\}] \subseteq ran +$
45	44 18	sstri	$⊢ + [X \times \{B\}] \subseteq On$
46	45	a1i	$⊢ φ \to + [X \times \{B\}] \subseteq On$
47	43 46	elpwd	$⊢ φ \to + [X \times \{B\}] \in 𝒫 On$
48	4 2	eqeltrrd	$⊢ φ \to ⋂ \{y \in On \| Y \subseteq y\} \in On$
49		onintrab2	$⊢ \exists y \in On Y \subseteq y \leftrightarrow ⋂ \{y \in On \| Y \subseteq y\} \in On$
50	48 49	sylibr	$⊢ φ \to \exists y \in On Y \subseteq y$
51		vex	$⊢ y \in V$
52	51	ssex	$⊢ Y \subseteq y \to Y \in V$
53	52	rexlimivw	$⊢ \exists y \in On Y \subseteq y \to Y \in V$
54	50 53	syl	$⊢ φ \to Y \in V$
55		xpexg	$⊢ (\{A\} \in V \land Y \in V) \to \{A\} \times Y \in V$
56	10 54 55	sylancr	$⊢ φ \to \{A\} \times Y \in V$
57		funimaexg	$⊢ (Fun + \land \{A\} \times Y \in V) \to + [\{A\} \times Y] \in V$
58	9 56 57	sylancr	$⊢ φ \to + [\{A\} \times Y] \in V$
59		imassrn	$⊢ + [\{A\} \times Y] \subseteq ran +$
60	59 18	sstri	$⊢ + [\{A\} \times Y] \subseteq On$
61	60	a1i	$⊢ φ \to + [\{A\} \times Y] \subseteq On$
62	58 61	elpwd	$⊢ φ \to + [\{A\} \times Y] \in 𝒫 On$
63		pwuncl	$⊢ (+ [X \times \{B\}] \in 𝒫 On \land + [\{A\} \times Y] \in 𝒫 On) \to + [X \times \{B\}] \cup + [\{A\} \times Y] \in 𝒫 On$
64	47 62 63	syl2anc	$⊢ φ \to + [X \times \{B\}] \cup + [\{A\} \times Y] \in 𝒫 On$
65	2 4	cofonr	$⊢ φ \to \forall q \in B \exists s \in Y q \subseteq s$
66		onss	$⊢ B \in On \to B \subseteq On$
67	2 66	syl	$⊢ φ \to B \subseteq On$
68	67	sselda	$⊢ (φ \land q \in B) \to q \in On$
69	68	adantr	$⊢ ((φ \land q \in B) \land s \in Y) \to q \in On$
70		onss	$⊢ y \in On \to y \subseteq On$
71	70	adantl	$⊢ (φ \land y \in On) \to y \subseteq On$
72		sstr	$⊢ (Y \subseteq y \land y \subseteq On) \to Y \subseteq On$
73	72	expcom	$⊢ y \subseteq On \to (Y \subseteq y \to Y \subseteq On)$
74	71 73	syl	$⊢ (φ \land y \in On) \to (Y \subseteq y \to Y \subseteq On)$
75	74	rexlimdva	$⊢ φ \to (\exists y \in On Y \subseteq y \to Y \subseteq On)$
76	50 75	mpd	$⊢ φ \to Y \subseteq On$
77	76	adantr	$⊢ (φ \land q \in B) \to Y \subseteq On$
78	77	sselda	$⊢ ((φ \land q \in B) \land s \in Y) \to s \in On$
79	1	ad2antrr	$⊢ ((φ \land q \in B) \land s \in Y) \to A \in On$
80		naddss2	$⊢ (q \in On \land s \in On \land A \in On) \to (q \subseteq s \leftrightarrow A + q \subseteq A + s)$
81	69 78 79 80	syl3anc	$⊢ ((φ \land q \in B) \land s \in Y) \to (q \subseteq s \leftrightarrow A + q \subseteq A + s)$
82	81	rexbidva	$⊢ (φ \land q \in B) \to (\exists s \in Y q \subseteq s \leftrightarrow \exists s \in Y A + q \subseteq A + s)$
83	82	ralbidva	$⊢ φ \to (\forall q \in B \exists s \in Y q \subseteq s \leftrightarrow \forall q \in B \exists s \in Y A + q \subseteq A + s)$
84	65 83	mpbid	$⊢ φ \to \forall q \in B \exists s \in Y A + q \subseteq A + s$
85	1	snssd	$⊢ φ \to \{A\} \subseteq On$
86		xpss12	$⊢ (\{A\} \subseteq On \land Y \subseteq On) \to \{A\} \times Y \subseteq On \times On$
87	85 76 86	syl2anc	$⊢ φ \to \{A\} \times Y \subseteq On \times On$
88		sseq2	$⊢ d = r + s \to (A + q \subseteq d \leftrightarrow A + q \subseteq r + s)$
89	88	imaeqexov	$⊢ (+ Fn (On \times On) \land \{A\} \times Y \subseteq On \times On) \to (\exists d \in + [\{A\} \times Y] A + q \subseteq d \leftrightarrow \exists r \in \{A\} \exists s \in Y A + q \subseteq r + s)$
90	7 87 89	sylancr	$⊢ φ \to (\exists d \in + [\{A\} \times Y] A + q \subseteq d \leftrightarrow \exists r \in \{A\} \exists s \in Y A + q \subseteq r + s)$
91		oveq1	$⊢ r = A \to r + s = A + s$
92	91	sseq2d	$⊢ r = A \to (A + q \subseteq r + s \leftrightarrow A + q \subseteq A + s)$
93	92	rexbidv	$⊢ r = A \to (\exists s \in Y A + q \subseteq r + s \leftrightarrow \exists s \in Y A + q \subseteq A + s)$
94	93	rexsng	$⊢ A \in On \to (\exists r \in \{A\} \exists s \in Y A + q \subseteq r + s \leftrightarrow \exists s \in Y A + q \subseteq A + s)$
95	1 94	syl	$⊢ φ \to (\exists r \in \{A\} \exists s \in Y A + q \subseteq r + s \leftrightarrow \exists s \in Y A + q \subseteq A + s)$
96	90 95	bitrd	$⊢ φ \to (\exists d \in + [\{A\} \times Y] A + q \subseteq d \leftrightarrow \exists s \in Y A + q \subseteq A + s)$
97	96	ralbidv	$⊢ φ \to (\forall q \in B \exists d \in + [\{A\} \times Y] A + q \subseteq d \leftrightarrow \forall q \in B \exists s \in Y A + q \subseteq A + s)$
98	84 97	mpbird	$⊢ φ \to \forall q \in B \exists d \in + [\{A\} \times Y] A + q \subseteq d$
99		olc	$⊢ \exists d \in + [\{A\} \times Y] A + q \subseteq d \to (\exists d \in + [X \times \{B\}] A + q \subseteq d \lor \exists d \in + [\{A\} \times Y] A + q \subseteq d)$
100	99	ralimi	$⊢ \forall q \in B \exists d \in + [\{A\} \times Y] A + q \subseteq d \to \forall q \in B (\exists d \in + [X \times \{B\}] A + q \subseteq d \lor \exists d \in + [\{A\} \times Y] A + q \subseteq d)$
101	98 100	syl	$⊢ φ \to \forall q \in B (\exists d \in + [X \times \{B\}] A + q \subseteq d \lor \exists d \in + [\{A\} \times Y] A + q \subseteq d)$
102		rexun	$⊢ \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d \leftrightarrow (\exists d \in + [X \times \{B\}] A + q \subseteq d \lor \exists d \in + [\{A\} \times Y] A + q \subseteq d)$
103	102	ralbii	$⊢ \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d \leftrightarrow \forall q \in B (\exists d \in + [X \times \{B\}] A + q \subseteq d \lor \exists d \in + [\{A\} \times Y] A + q \subseteq d)$
104	101 103	sylibr	$⊢ φ \to \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d$
105		xpss12	$⊢ (\{A\} \subseteq On \land B \subseteq On) \to \{A\} \times B \subseteq On \times On$
106	85 67 105	syl2anc	$⊢ φ \to \{A\} \times B \subseteq On \times On$
107		sseq1	$⊢ c = p + q \to (c \subseteq d \leftrightarrow p + q \subseteq d)$
108	107	rexbidv	$⊢ c = p + q \to (\exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d)$
109	108	imaeqalov	$⊢ (+ Fn (On \times On) \land \{A\} \times B \subseteq On \times On) \to (\forall c \in + [\{A\} \times B] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow \forall p \in \{A\} \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d)$
110	7 106 109	sylancr	$⊢ φ \to (\forall c \in + [\{A\} \times B] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow \forall p \in \{A\} \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d)$
111		oveq1	$⊢ p = A \to p + q = A + q$
112	111	sseq1d	$⊢ p = A \to (p + q \subseteq d \leftrightarrow A + q \subseteq d)$
113	112	rexbidv	$⊢ p = A \to (\exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d)$
114	113	ralbidv	$⊢ p = A \to (\forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d)$
115	114	ralsng	$⊢ A \in On \to (\forall p \in \{A\} \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d)$
116	1 115	syl	$⊢ φ \to (\forall p \in \{A\} \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d)$
117	110 116	bitrd	$⊢ φ \to (\forall c \in + [\{A\} \times B] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow \forall q \in B \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) A + q \subseteq d)$
118	104 117	mpbird	$⊢ φ \to \forall c \in + [\{A\} \times B] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d$
119	1 3	cofonr	$⊢ φ \to \forall p \in A \exists r \in X p \subseteq r$
120		onss	$⊢ A \in On \to A \subseteq On$
121	1 120	syl	$⊢ φ \to A \subseteq On$
122	121	sselda	$⊢ (φ \land p \in A) \to p \in On$
123	122	adantr	$⊢ ((φ \land p \in A) \land r \in X) \to p \in On$
124		ssintub	$⊢ X \subseteq ⋂ \{x \in On \| X \subseteq x\}$
125	3 121	eqsstrrd	$⊢ φ \to ⋂ \{x \in On \| X \subseteq x\} \subseteq On$
126	124 125	sstrid	$⊢ φ \to X \subseteq On$
127	126	adantr	$⊢ (φ \land p \in A) \to X \subseteq On$
128	127	sselda	$⊢ ((φ \land p \in A) \land r \in X) \to r \in On$
129	2	ad2antrr	$⊢ ((φ \land p \in A) \land r \in X) \to B \in On$
130		naddss1	$⊢ (p \in On \land r \in On \land B \in On) \to (p \subseteq r \leftrightarrow p + B \subseteq r + B)$
131	123 128 129 130	syl3anc	$⊢ ((φ \land p \in A) \land r \in X) \to (p \subseteq r \leftrightarrow p + B \subseteq r + B)$
132	131	rexbidva	$⊢ (φ \land p \in A) \to (\exists r \in X p \subseteq r \leftrightarrow \exists r \in X p + B \subseteq r + B)$
133	132	ralbidva	$⊢ φ \to (\forall p \in A \exists r \in X p \subseteq r \leftrightarrow \forall p \in A \exists r \in X p + B \subseteq r + B)$
134	119 133	mpbid	$⊢ φ \to \forall p \in A \exists r \in X p + B \subseteq r + B$
135	2	snssd	$⊢ φ \to \{B\} \subseteq On$
136		xpss12	$⊢ (X \subseteq On \land \{B\} \subseteq On) \to X \times \{B\} \subseteq On \times On$
137	126 135 136	syl2anc	$⊢ φ \to X \times \{B\} \subseteq On \times On$
138		sseq2	$⊢ d = r + s \to (p + B \subseteq d \leftrightarrow p + B \subseteq r + s)$
139	138	imaeqexov	$⊢ (+ Fn (On \times On) \land X \times \{B\} \subseteq On \times On) \to (\exists d \in + [X \times \{B\}] p + B \subseteq d \leftrightarrow \exists r \in X \exists s \in \{B\} p + B \subseteq r + s)$
140	7 137 139	sylancr	$⊢ φ \to (\exists d \in + [X \times \{B\}] p + B \subseteq d \leftrightarrow \exists r \in X \exists s \in \{B\} p + B \subseteq r + s)$
141		oveq2	$⊢ s = B \to r + s = r + B$
142	141	sseq2d	$⊢ s = B \to (p + B \subseteq r + s \leftrightarrow p + B \subseteq r + B)$
143	142	rexsng	$⊢ B \in On \to (\exists s \in \{B\} p + B \subseteq r + s \leftrightarrow p + B \subseteq r + B)$
144	2 143	syl	$⊢ φ \to (\exists s \in \{B\} p + B \subseteq r + s \leftrightarrow p + B \subseteq r + B)$
145	144	rexbidv	$⊢ φ \to (\exists r \in X \exists s \in \{B\} p + B \subseteq r + s \leftrightarrow \exists r \in X p + B \subseteq r + B)$
146	140 145	bitrd	$⊢ φ \to (\exists d \in + [X \times \{B\}] p + B \subseteq d \leftrightarrow \exists r \in X p + B \subseteq r + B)$
147	146	ralbidv	$⊢ φ \to (\forall p \in A \exists d \in + [X \times \{B\}] p + B \subseteq d \leftrightarrow \forall p \in A \exists r \in X p + B \subseteq r + B)$
148	134 147	mpbird	$⊢ φ \to \forall p \in A \exists d \in + [X \times \{B\}] p + B \subseteq d$
149		orc	$⊢ \exists d \in + [X \times \{B\}] p + B \subseteq d \to (\exists d \in + [X \times \{B\}] p + B \subseteq d \lor \exists d \in + [\{A\} \times Y] p + B \subseteq d)$
150	149	ralimi	$⊢ \forall p \in A \exists d \in + [X \times \{B\}] p + B \subseteq d \to \forall p \in A (\exists d \in + [X \times \{B\}] p + B \subseteq d \lor \exists d \in + [\{A\} \times Y] p + B \subseteq d)$
151	148 150	syl	$⊢ φ \to \forall p \in A (\exists d \in + [X \times \{B\}] p + B \subseteq d \lor \exists d \in + [\{A\} \times Y] p + B \subseteq d)$
152		rexun	$⊢ \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d \leftrightarrow (\exists d \in + [X \times \{B\}] p + B \subseteq d \lor \exists d \in + [\{A\} \times Y] p + B \subseteq d)$
153	152	ralbii	$⊢ \forall p \in A \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d \leftrightarrow \forall p \in A (\exists d \in + [X \times \{B\}] p + B \subseteq d \lor \exists d \in + [\{A\} \times Y] p + B \subseteq d)$
154	151 153	sylibr	$⊢ φ \to \forall p \in A \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d$
155		oveq2	$⊢ q = B \to p + q = p + B$
156	155	sseq1d	$⊢ q = B \to (p + q \subseteq d \leftrightarrow p + B \subseteq d)$
157	156	rexbidv	$⊢ q = B \to (\exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d)$
158	157	ralsng	$⊢ B \in On \to (\forall q \in \{B\} \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d)$
159	2 158	syl	$⊢ φ \to (\forall q \in \{B\} \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d)$
160	159	ralbidv	$⊢ φ \to (\forall p \in A \forall q \in \{B\} \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d \leftrightarrow \forall p \in A \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + B \subseteq d)$
161	154 160	mpbird	$⊢ φ \to \forall p \in A \forall q \in \{B\} \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d$
162		xpss12	$⊢ (A \subseteq On \land \{B\} \subseteq On) \to A \times \{B\} \subseteq On \times On$
163	121 135 162	syl2anc	$⊢ φ \to A \times \{B\} \subseteq On \times On$
164	108	imaeqalov	$⊢ (+ Fn (On \times On) \land A \times \{B\} \subseteq On \times On) \to (\forall c \in + [A \times \{B\}] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow \forall p \in A \forall q \in \{B\} \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d)$
165	7 163 164	sylancr	$⊢ φ \to (\forall c \in + [A \times \{B\}] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow \forall p \in A \forall q \in \{B\} \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) p + q \subseteq d)$
166	161 165	mpbird	$⊢ φ \to \forall c \in + [A \times \{B\}] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d$
167		ralunb	$⊢ \forall c \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \leftrightarrow (\forall c \in + [\{A\} \times B] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d \land \forall c \in + [A \times \{B\}] \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d)$
168	118 166 167	sylanbrc	$⊢ φ \to \forall c \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) \exists d \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) c \subseteq d$
169	124 3	sseqtrrid	$⊢ φ \to X \subseteq A$
170	169	sselda	$⊢ (φ \land p \in X) \to p \in A$
171		ssid	$⊢ p \subseteq p$
172		sseq2	$⊢ r = p \to (p \subseteq r \leftrightarrow p \subseteq p)$
173	172	rspcev	$⊢ (p \in A \land p \subseteq p) \to \exists r \in A p \subseteq r$
174	170 171 173	sylancl	$⊢ (φ \land p \in X) \to \exists r \in A p \subseteq r$
175	174	ralrimiva	$⊢ φ \to \forall p \in X \exists r \in A p \subseteq r$
176	126	sselda	$⊢ (φ \land p \in X) \to p \in On$
177	176	adantr	$⊢ ((φ \land p \in X) \land r \in A) \to p \in On$
178	121	adantr	$⊢ (φ \land p \in X) \to A \subseteq On$
179	178	sselda	$⊢ ((φ \land p \in X) \land r \in A) \to r \in On$
180	2	ad2antrr	$⊢ ((φ \land p \in X) \land r \in A) \to B \in On$
181	177 179 180 130	syl3anc	$⊢ ((φ \land p \in X) \land r \in A) \to (p \subseteq r \leftrightarrow p + B \subseteq r + B)$
182	181	rexbidva	$⊢ (φ \land p \in X) \to (\exists r \in A p \subseteq r \leftrightarrow \exists r \in A p + B \subseteq r + B)$
183	182	ralbidva	$⊢ φ \to (\forall p \in X \exists r \in A p \subseteq r \leftrightarrow \forall p \in X \exists r \in A p + B \subseteq r + B)$
184	175 183	mpbid	$⊢ φ \to \forall p \in X \exists r \in A p + B \subseteq r + B$
185		sseq2	$⊢ b = r + s \to (p + B \subseteq b \leftrightarrow p + B \subseteq r + s)$
186	185	imaeqexov	$⊢ (+ Fn (On \times On) \land A \times \{B\} \subseteq On \times On) \to (\exists b \in + [A \times \{B\}] p + B \subseteq b \leftrightarrow \exists r \in A \exists s \in \{B\} p + B \subseteq r + s)$
187	7 163 186	sylancr	$⊢ φ \to (\exists b \in + [A \times \{B\}] p + B \subseteq b \leftrightarrow \exists r \in A \exists s \in \{B\} p + B \subseteq r + s)$
188	144	rexbidv	$⊢ φ \to (\exists r \in A \exists s \in \{B\} p + B \subseteq r + s \leftrightarrow \exists r \in A p + B \subseteq r + B)$
189	187 188	bitrd	$⊢ φ \to (\exists b \in + [A \times \{B\}] p + B \subseteq b \leftrightarrow \exists r \in A p + B \subseteq r + B)$
190	189	ralbidv	$⊢ φ \to (\forall p \in X \exists b \in + [A \times \{B\}] p + B \subseteq b \leftrightarrow \forall p \in X \exists r \in A p + B \subseteq r + B)$
191	184 190	mpbird	$⊢ φ \to \forall p \in X \exists b \in + [A \times \{B\}] p + B \subseteq b$
192		olc	$⊢ \exists b \in + [A \times \{B\}] p + B \subseteq b \to (\exists b \in + [\{A\} \times B] p + B \subseteq b \lor \exists b \in + [A \times \{B\}] p + B \subseteq b)$
193	192	ralimi	$⊢ \forall p \in X \exists b \in + [A \times \{B\}] p + B \subseteq b \to \forall p \in X (\exists b \in + [\{A\} \times B] p + B \subseteq b \lor \exists b \in + [A \times \{B\}] p + B \subseteq b)$
194	191 193	syl	$⊢ φ \to \forall p \in X (\exists b \in + [\{A\} \times B] p + B \subseteq b \lor \exists b \in + [A \times \{B\}] p + B \subseteq b)$
195	155	sseq1d	$⊢ q = B \to (p + q \subseteq b \leftrightarrow p + B \subseteq b)$
196	195	rexbidv	$⊢ q = B \to (\exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + B \subseteq b)$
197	196	ralsng	$⊢ B \in On \to (\forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + B \subseteq b)$
198	2 197	syl	$⊢ φ \to (\forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + B \subseteq b)$
199	198	adantr	$⊢ (φ \land p \in X) \to (\forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + B \subseteq b)$
200		rexun	$⊢ \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + B \subseteq b \leftrightarrow (\exists b \in + [\{A\} \times B] p + B \subseteq b \lor \exists b \in + [A \times \{B\}] p + B \subseteq b)$
201	199 200	bitrdi	$⊢ (φ \land p \in X) \to (\forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow (\exists b \in + [\{A\} \times B] p + B \subseteq b \lor \exists b \in + [A \times \{B\}] p + B \subseteq b))$
202	201	ralbidva	$⊢ φ \to (\forall p \in X \forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \forall p \in X (\exists b \in + [\{A\} \times B] p + B \subseteq b \lor \exists b \in + [A \times \{B\}] p + B \subseteq b))$
203	194 202	mpbird	$⊢ φ \to \forall p \in X \forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b$
204		sseq1	$⊢ a = p + q \to (a \subseteq b \leftrightarrow p + q \subseteq b)$
205	204	rexbidv	$⊢ a = p + q \to (\exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \leftrightarrow \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b)$
206	205	imaeqalov	$⊢ (+ Fn (On \times On) \land X \times \{B\} \subseteq On \times On) \to (\forall a \in + [X \times \{B\}] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \leftrightarrow \forall p \in X \forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b)$
207	7 137 206	sylancr	$⊢ φ \to (\forall a \in + [X \times \{B\}] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \leftrightarrow \forall p \in X \forall q \in \{B\} \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b)$
208	203 207	mpbird	$⊢ φ \to \forall a \in + [X \times \{B\}] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b$
209		ssintub	$⊢ Y \subseteq ⋂ \{y \in On \| Y \subseteq y\}$
210	209 4	sseqtrrid	$⊢ φ \to Y \subseteq B$
211	210	sselda	$⊢ (φ \land q \in Y) \to q \in B$
212		ssid	$⊢ q \subseteq q$
213		sseq2	$⊢ s = q \to (q \subseteq s \leftrightarrow q \subseteq q)$
214	213	rspcev	$⊢ (q \in B \land q \subseteq q) \to \exists s \in B q \subseteq s$
215	211 212 214	sylancl	$⊢ (φ \land q \in Y) \to \exists s \in B q \subseteq s$
216	215	ralrimiva	$⊢ φ \to \forall q \in Y \exists s \in B q \subseteq s$
217	92	rexbidv	$⊢ r = A \to (\exists s \in B A + q \subseteq r + s \leftrightarrow \exists s \in B A + q \subseteq A + s)$
218	217	rexsng	$⊢ A \in On \to (\exists r \in \{A\} \exists s \in B A + q \subseteq r + s \leftrightarrow \exists s \in B A + q \subseteq A + s)$
219	1 218	syl	$⊢ φ \to (\exists r \in \{A\} \exists s \in B A + q \subseteq r + s \leftrightarrow \exists s \in B A + q \subseteq A + s)$
220	219	adantr	$⊢ (φ \land q \in Y) \to (\exists r \in \{A\} \exists s \in B A + q \subseteq r + s \leftrightarrow \exists s \in B A + q \subseteq A + s)$
221		sseq2	$⊢ b = r + s \to (A + q \subseteq b \leftrightarrow A + q \subseteq r + s)$
222	221	imaeqexov	$⊢ (+ Fn (On \times On) \land \{A\} \times B \subseteq On \times On) \to (\exists b \in + [\{A\} \times B] A + q \subseteq b \leftrightarrow \exists r \in \{A\} \exists s \in B A + q \subseteq r + s)$
223	7 106 222	sylancr	$⊢ φ \to (\exists b \in + [\{A\} \times B] A + q \subseteq b \leftrightarrow \exists r \in \{A\} \exists s \in B A + q \subseteq r + s)$
224	223	adantr	$⊢ (φ \land q \in Y) \to (\exists b \in + [\{A\} \times B] A + q \subseteq b \leftrightarrow \exists r \in \{A\} \exists s \in B A + q \subseteq r + s)$
225	76	sselda	$⊢ (φ \land q \in Y) \to q \in On$
226	225	adantr	$⊢ ((φ \land q \in Y) \land s \in B) \to q \in On$
227	67	adantr	$⊢ (φ \land q \in Y) \to B \subseteq On$
228	227	sselda	$⊢ ((φ \land q \in Y) \land s \in B) \to s \in On$
229	1	ad2antrr	$⊢ ((φ \land q \in Y) \land s \in B) \to A \in On$
230	226 228 229 80	syl3anc	$⊢ ((φ \land q \in Y) \land s \in B) \to (q \subseteq s \leftrightarrow A + q \subseteq A + s)$
231	230	rexbidva	$⊢ (φ \land q \in Y) \to (\exists s \in B q \subseteq s \leftrightarrow \exists s \in B A + q \subseteq A + s)$
232	220 224 231	3bitr4d	$⊢ (φ \land q \in Y) \to (\exists b \in + [\{A\} \times B] A + q \subseteq b \leftrightarrow \exists s \in B q \subseteq s)$
233	232	ralbidva	$⊢ φ \to (\forall q \in Y \exists b \in + [\{A\} \times B] A + q \subseteq b \leftrightarrow \forall q \in Y \exists s \in B q \subseteq s)$
234	216 233	mpbird	$⊢ φ \to \forall q \in Y \exists b \in + [\{A\} \times B] A + q \subseteq b$
235		orc	$⊢ \exists b \in + [\{A\} \times B] A + q \subseteq b \to (\exists b \in + [\{A\} \times B] A + q \subseteq b \lor \exists b \in + [A \times \{B\}] A + q \subseteq b)$
236	235	ralimi	$⊢ \forall q \in Y \exists b \in + [\{A\} \times B] A + q \subseteq b \to \forall q \in Y (\exists b \in + [\{A\} \times B] A + q \subseteq b \lor \exists b \in + [A \times \{B\}] A + q \subseteq b)$
237	234 236	syl	$⊢ φ \to \forall q \in Y (\exists b \in + [\{A\} \times B] A + q \subseteq b \lor \exists b \in + [A \times \{B\}] A + q \subseteq b)$
238		rexun	$⊢ \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b \leftrightarrow (\exists b \in + [\{A\} \times B] A + q \subseteq b \lor \exists b \in + [A \times \{B\}] A + q \subseteq b)$
239	238	ralbii	$⊢ \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b \leftrightarrow \forall q \in Y (\exists b \in + [\{A\} \times B] A + q \subseteq b \lor \exists b \in + [A \times \{B\}] A + q \subseteq b)$
240	237 239	sylibr	$⊢ φ \to \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b$
241	111	sseq1d	$⊢ p = A \to (p + q \subseteq b \leftrightarrow A + q \subseteq b)$
242	241	rexbidv	$⊢ p = A \to (\exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b)$
243	242	ralbidv	$⊢ p = A \to (\forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b)$
244	243	ralsng	$⊢ A \in On \to (\forall p \in \{A\} \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b)$
245	1 244	syl	$⊢ φ \to (\forall p \in \{A\} \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b \leftrightarrow \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) A + q \subseteq b)$
246	240 245	mpbird	$⊢ φ \to \forall p \in \{A\} \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b$
247	205	imaeqalov	$⊢ (+ Fn (On \times On) \land \{A\} \times Y \subseteq On \times On) \to (\forall a \in + [\{A\} \times Y] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \leftrightarrow \forall p \in \{A\} \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b)$
248	7 87 247	sylancr	$⊢ φ \to (\forall a \in + [\{A\} \times Y] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \leftrightarrow \forall p \in \{A\} \forall q \in Y \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) p + q \subseteq b)$
249	246 248	mpbird	$⊢ φ \to \forall a \in + [\{A\} \times Y] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b$
250		ralunb	$⊢ \forall a \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \leftrightarrow (\forall a \in + [X \times \{B\}] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b \land \forall a \in + [\{A\} \times Y] \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b)$
251	208 249 250	sylanbrc	$⊢ φ \to \forall a \in (+ [X \times \{B\}] \cup + [\{A\} \times Y]) \exists b \in (+ [\{A\} \times B] \cup + [A \times \{B\}]) a \subseteq b$
252	32 64 168 251	cofon2	$⊢ φ \to ⋂ \{w \in On \| + [\{A\} \times B] \cup + [A \times \{B\}] \subseteq w\} = ⋂ \{z \in On \| + [X \times \{B\}] \cup + [\{A\} \times Y] \subseteq z\}$
253	6 252	eqtrd	$⊢ φ \to A + B = ⋂ \{z \in On \| + [X \times \{B\}] \cup + [\{A\} \times Y] \subseteq z\}$

Metamath Proof Explorer

Theorem naddunif

Proof