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 8170

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 5627	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		sopo 5627	. . 3 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
3		soxp.1	. . . 4 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
4	3	poxp 8169	. . 3 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
5	1, 2, 4	syl2an 595	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6		elxp 5723	. . . . 5 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
7		elxp 5723	. . . . 5 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
8		ioran 984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
9		ioran 984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))
10		ianor 982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
11	10	anbi2i 622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
12	9, 11	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13		ianor 982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
14	12, 13	anbi12i 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
15	8, 14	bitri 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16		solin 5634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎))
17		3orass 1090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
18		df-or 847	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
19	17, 18	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
20	16, 19	sylib 218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
21		solin 5634	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))
22		3orass 1090	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
23		df-or 847	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
24	22, 23	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
25	21, 24	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
26	25	orim2d 967	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))))
27	20, 26	im2anan9 619	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))))
28		pm2.53 850	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → 𝑐𝑅𝑎))
29		orc 866	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
30	28, 29	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
31	30	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
32		orel1 887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑏 = 𝑑 → ((𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
33	32	orim2d 967	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)))
34	33	anim2d 611	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑏 = 𝑑 → (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))))
35		imor 852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 → 𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))
36	35	biimpri 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑎 = 𝑐 → 𝑑𝑆𝑏))
37	36	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38		equcomi 2016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → 𝑐 = 𝑎)
39	38	anim1i 614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))
40	39	olcd 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
41	40	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
42	37, 41	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
43	29	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
44	42, 43	jaoi 856	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
45	44	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
46	34, 45	syl6com 37	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
47	31, 46	jaod 858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
48	27, 47	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
49	48	impd 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
50	15, 49	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
51		df-3or 1088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
52		df-or 847	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
53	51, 52	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
54	50, 53	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
55		pm3.2 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
56	55	ad2ant2l 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
57		idd 24	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
58		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴))
59	58	ancomd 461	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴))
60		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))
61	60	ancomd 461	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))
62		pm3.2 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
63	59, 61, 62	syl2an 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
64	56, 57, 63	3orim123d 1444	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
65	54, 64	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
66	65	an4s 659	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
67	66	expcom 413	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
68	67	an4s 659	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
69		breq12 5171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
70		eqeq12 2757	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71		breq12 5171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
72	71	ancoms 458	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
73	69, 70, 72	3orbi123d 1435	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
74	3	xporderlem 8168	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
75		vex 3492	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ V
76		vex 3492	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
77	75, 76	opth 5496	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
78	3	xporderlem 8168	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
79	74, 77, 78	3orbi123i 1156	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
80	73, 79	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
81	80	biimprcd 250	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
82	68, 81	syl6 35	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
83	82	com3r 87	. . . . . . . . . . . 12 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
84	83	imp 406	. . . . . . . . . . 11 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
85	84	an4s 659	. . . . . . . . . 10 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
86	85	expcom 413	. . . . . . . . 9 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
87	86	exlimivv 1931	. . . . . . . 8 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
88	87	com12 32	. . . . . . 7 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
89	88	exlimivv 1931	. . . . . 6 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
90	89	imp 406	. . . . 5 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
91	6, 7, 90	syl2anb 597	. . . 4 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
92	91	com12 32	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
93	92	ralrimivv 3206	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))
94		df-so 5608	. 2 ⊢ (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
95	5, 93, 94	sylanbrc 582	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∨ w3o 1086 = wceq 1537 ∃wex 1777 ∈ wcel 2108 ∀wral 3067 ⟨cop 4654 class class class wbr 5166 {copab 5228 Po wpo 5605 Or wor 5606 × cxp 5698 ‘cfv 6573 1^st c1st 8028 2^nd c2nd 8029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-po 5607 df-so 5608 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-iota 6525 df-fun 6575 df-fv 6581 df-1st 8030 df-2nd 8031

This theorem is referenced by: wexp 8171 rrx2plordso 48458

W3C validator