soxp - Metamath Proof Explorer

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

Theorem soxp 7874

Description: A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)

**Hypothesis**
Ref	Expression
soxp.1	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}

**Assertion**
Ref	Expression
soxp	⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝑅,𝑦 𝑥,𝑆,𝑦 Allowed substitution hints: 𝑇(𝑥,𝑦)

Proof of Theorem soxp Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sopo 5472	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		sopo 5472	. . 3 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
3		soxp.1	. . . 4 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
4	3	poxp 7873	. . 3 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
5	1, 2, 4	syl2an 599	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6		elxp 5559	. . . . 5 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
7		elxp 5559	. . . . 5 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
8		ioran 984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
9		ioran 984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))
10		ianor 982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
11	10	anbi2i 626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
12	9, 11	bitri 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13		ianor 982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
14	12, 13	anbi12i 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
15	8, 14	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16		solin 5478	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎))
17		3orass 1092	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
18		df-or 848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
19	17, 18	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
20	16, 19	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
21		solin 5478	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))
22		3orass 1092	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
23		df-or 848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
24	22, 23	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
25	21, 24	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
26	25	orim2d 967	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))))
27	20, 26	im2anan9 623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))))
28		pm2.53 851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → 𝑐𝑅𝑎))
29		orc 867	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
30	28, 29	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
31	30	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
32		orel1 889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑏 = 𝑑 → ((𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
33	32	orim2d 967	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)))
34	33	anim2d 615	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑏 = 𝑑 → (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))))
35		imor 853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 → 𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))
36	35	biimpri 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑎 = 𝑐 → 𝑑𝑆𝑏))
37	36	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38		equcomi 2027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → 𝑐 = 𝑎)
39	38	anim1i 618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))
40	39	olcd 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
41	40	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
42	37, 41	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
43	29	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
44	42, 43	jaoi 857	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
45	44	imp 410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
46	34, 45	syl6com 37	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
47	31, 46	jaod 859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
48	27, 47	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
49	48	impd 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
50	15, 49	syl5bi 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
51		df-3or 1090	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
52		df-or 848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
53	51, 52	bitri 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
54	50, 53	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
55		pm3.2 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
56	55	ad2ant2l 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
57		idd 24	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
58		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴))
59	58	ancomd 465	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴))
60		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))
61	60	ancomd 465	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))
62		pm3.2 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
63	59, 61, 62	syl2an 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
64	56, 57, 63	3orim123d 1446	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
65	54, 64	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
66	65	an4s 660	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
67	66	expcom 417	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
68	67	an4s 660	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
69		breq12 5044	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
70		eqeq12 2750	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71		breq12 5044	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
72	71	ancoms 462	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
73	69, 70, 72	3orbi123d 1437	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
74	3	xporderlem 7872	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
75		vex 3402	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ V
76		vex 3402	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
77	75, 76	opth 5345	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
78	3	xporderlem 7872	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
79	74, 77, 78	3orbi123i 1158	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
80	73, 79	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
81	80	biimprcd 253	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
82	68, 81	syl6 35	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
83	82	com3r 87	. . . . . . . . . . . 12 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
84	83	imp 410	. . . . . . . . . . 11 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
85	84	an4s 660	. . . . . . . . . 10 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
86	85	expcom 417	. . . . . . . . 9 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
87	86	exlimivv 1940	. . . . . . . 8 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
88	87	com12 32	. . . . . . 7 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
89	88	exlimivv 1940	. . . . . 6 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
90	89	imp 410	. . . . 5 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
91	6, 7, 90	syl2anb 601	. . . 4 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
92	91	com12 32	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
93	92	ralrimivv 3101	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))
94		df-so 5454	. 2 ⊢ (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
95	5, 93, 94	sylanbrc 586	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 847 ∨ w3o 1088 = wceq 1543 ∃wex 1787 ∈ wcel 2112 ∀wral 3051 ⟨cop 4533 class class class wbr 5039 {copab 5101 Po wpo 5451 Or wor 5452 × cxp 5534 ‘cfv 6358 1^st c1st 7737 2^nd c2nd 7738

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 ax-un 7501

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-sbc 3684 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-opab 5102 df-mpt 5121 df-id 5440 df-po 5453 df-so 5454 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-iota 6316 df-fun 6360 df-fv 6366 df-1st 7739 df-2nd 7740

This theorem is referenced by: wexp 7875 rrx2plordso 45686

W3C validator