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 7970

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 5522	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		sopo 5522	. . 3 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
3		soxp.1	. . . 4 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
4	3	poxp 7969	. . 3 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
5	1, 2, 4	syl2an 596	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6		elxp 5612	. . . . 5 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
7		elxp 5612	. . . . 5 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
8		ioran 981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
9		ioran 981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))
10		ianor 979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
11	10	anbi2i 623	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
12	9, 11	bitri 274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13		ianor 979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
14	12, 13	anbi12i 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
15	8, 14	bitri 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16		solin 5528	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎))
17		3orass 1089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
18		df-or 845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
19	17, 18	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
20	16, 19	sylib 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
21		solin 5528	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))
22		3orass 1089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
23		df-or 845	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
24	22, 23	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
25	21, 24	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
26	25	orim2d 964	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))))
27	20, 26	im2anan9 620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))))
28		pm2.53 848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → 𝑐𝑅𝑎))
29		orc 864	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
30	28, 29	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
31	30	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
32		orel1 886	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑏 = 𝑑 → ((𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
33	32	orim2d 964	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)))
34	33	anim2d 612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑏 = 𝑑 → (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))))
35		imor 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 → 𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))
36	35	biimpri 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑎 = 𝑐 → 𝑑𝑆𝑏))
37	36	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38		equcomi 2020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → 𝑐 = 𝑎)
39	38	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))
40	39	olcd 871	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
41	40	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
42	37, 41	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
43	29	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
44	42, 43	jaoi 854	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
45	44	imp 407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
46	34, 45	syl6com 37	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
47	31, 46	jaod 856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
48	27, 47	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
49	48	impd 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
50	15, 49	syl5bi 241	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
51		df-3or 1087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
52		df-or 845	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
53	51, 52	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
54	50, 53	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
55		pm3.2 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
56	55	ad2ant2l 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
57		idd 24	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
58		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴))
59	58	ancomd 462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴))
60		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))
61	60	ancomd 462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))
62		pm3.2 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
63	59, 61, 62	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
64	56, 57, 63	3orim123d 1443	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
65	54, 64	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
66	65	an4s 657	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
67	66	expcom 414	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
68	67	an4s 657	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
69		breq12 5079	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
70		eqeq12 2755	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71		breq12 5079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
72	71	ancoms 459	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
73	69, 70, 72	3orbi123d 1434	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
74	3	xporderlem 7968	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
75		vex 3436	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ V
76		vex 3436	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
77	75, 76	opth 5391	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
78	3	xporderlem 7968	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
79	74, 77, 78	3orbi123i 1155	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
80	73, 79	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
81	80	biimprcd 249	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
82	68, 81	syl6 35	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
83	82	com3r 87	. . . . . . . . . . . 12 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
84	83	imp 407	. . . . . . . . . . 11 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
85	84	an4s 657	. . . . . . . . . 10 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
86	85	expcom 414	. . . . . . . . 9 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
87	86	exlimivv 1935	. . . . . . . 8 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
88	87	com12 32	. . . . . . 7 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
89	88	exlimivv 1935	. . . . . 6 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
90	89	imp 407	. . . . 5 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
91	6, 7, 90	syl2anb 598	. . . 4 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
92	91	com12 32	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
93	92	ralrimivv 3122	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))
94		df-so 5504	. 2 ⊢ (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
95	5, 93, 94	sylanbrc 583	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∨ w3o 1085 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ∀wral 3064 ⟨cop 4567 class class class wbr 5074 {copab 5136 Po wpo 5501 Or wor 5502 × cxp 5587 ‘cfv 6433 1^st c1st 7829 2^nd c2nd 7830

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-po 5503 df-so 5504 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-iota 6391 df-fun 6435 df-fv 6441 df-1st 7831 df-2nd 7832

This theorem is referenced by: wexp 7971 rrx2plordso 46070

W3C validator