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 7177

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 4976	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		sopo 4976	. . 3 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
3		soxp.1	. . . 4 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
4	3	poxp 7176	. . 3 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
5	1, 2, 4	syl2an 493	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6		elxp 5055	. . . . 5 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
7		elxp 5055	. . . . 5 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
8		ioran 510	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
9		ioran 510	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))
10		ianor 508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
11	10	anbi2i 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
12	9, 11	bitri 263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13		ianor 508	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
14	12, 13	anbi12i 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
15	8, 14	bitri 263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16		solin 4982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎))
17		3orass 1034	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
18		df-or 384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
19	17, 18	bitri 263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
20	16, 19	sylib 207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
21		solin 4982	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))
22		3orass 1034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
23		df-or 384	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
24	22, 23	bitri 263	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
25	21, 24	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
26	25	orim2d 881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))))
27	20, 26	im2anan9 876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))))
28		pm2.53 387	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → 𝑐𝑅𝑎))
29		orc 399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
30	28, 29	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
31	30	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
32		orel1 396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑏 = 𝑑 → ((𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
33	32	orim2d 881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)))
34	33	anim2d 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑏 = 𝑑 → (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))))
35		imor 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 → 𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))
36	35	biimpri 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑎 = 𝑐 → 𝑑𝑆𝑏))
37	36	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38		equcomi 1931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → 𝑐 = 𝑎)
39	38	anim1i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))
40	39	olcd 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
41	40	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
42	37, 41	syld 46	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
43	29	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
44	42, 43	jaoi 393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
45	44	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
46	34, 45	syl6com 36	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
47	31, 46	jaod 394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
48	27, 47	syl6 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
49	48	impd 446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
50	15, 49	syl5bi 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
51		df-3or 1032	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
52		df-or 384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
53	51, 52	bitri 263	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
54	50, 53	sylibr 223	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
55		pm3.2 462	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
56	55	ad2ant2l 778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
57		idd 24	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
58		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴))
59	58	ancomd 466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴))
60		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))
61	60	ancomd 466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))
62		pm3.2 462	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
63	59, 61, 62	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)) → (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
64	56, 57, 63	3orim123d 1399	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
65	54, 64	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
66	65	an4s 865	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
67	66	expcom 450	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
68	67	an4s 865	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
69		breq12 4588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
70		eqeq12 2623	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71		breq12 4588	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
72	71	ancoms 468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
73	69, 70, 72	3orbi123d 1390	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
74	3	xporderlem 7175	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
75		vex 3176	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ V
76		vex 3176	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
77	75, 76	opth 4871	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
78	3	xporderlem 7175	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
79	74, 77, 78	3orbi123i 1245	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))))
80	73, 79	syl6bb 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
81	80	biimprcd 239	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
82	68, 81	syl6 34	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
83	82	com3r 85	. . . . . . . . . . . 12 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
84	83	imp 444	. . . . . . . . . . 11 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
85	84	an4s 865	. . . . . . . . . 10 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
86	85	expcom 450	. . . . . . . . 9 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
87	86	exlimivv 1847	. . . . . . . 8 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
88	87	com12 32	. . . . . . 7 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
89	88	exlimivv 1847	. . . . . 6 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
90	89	imp 444	. . . . 5 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
91	6, 7, 90	syl2anb 495	. . . 4 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
92	91	com12 32	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
93	92	ralrimivv 2953	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))
94		df-so 4960	. 2 ⊢ (𝑇 Or (𝐴 × 𝐵) ↔ (𝑇 Po (𝐴 × 𝐵) ∧ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
95	5, 93, 94	sylanbrc 695	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∨ w3o 1030 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∀wral 2896 ⟨cop 4131 class class class wbr 4583 {copab 4642 Po wpo 4957 Or wor 4958 × cxp 5036 ‘cfv 5804 1^st c1st 7057 2^nd c2nd 7058

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-po 4959 df-so 4960 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-iota 5768 df-fun 5806 df-fv 5812 df-1st 7059 df-2nd 7060

This theorem is referenced by: wexp 7178

W3C validator