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 8126

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 5580	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		sopo 5580	. . 3 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
3		soxp.1	. . . 4 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
4	3	poxp 8125	. . 3 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
5	1, 2, 4	syl2an 596	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Po (𝐴 × 𝐵))
6		elxp 5677	. . . . 5 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
7		elxp 5677	. . . . 5 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
8		ioran 985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)))
9		ioran 985	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))
10		ianor 983	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑))
11	10	anbi2i 623	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((¬ 𝑎𝑅𝑐 ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
12	9, 11	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ↔ (¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)))
13		ianor 983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑))
14	12, 13	anbi12i 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ ¬ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
15	8, 14	bitri 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ↔ ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑)))
16		solin 5588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎))
17		3orass 1089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
18		df-or 848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
19	17, 18	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ↔ (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
20	16, 19	sylib 218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (¬ 𝑎𝑅𝑐 → (𝑎 = 𝑐 ∨ 𝑐𝑅𝑎)))
21		solin 5588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))
22		3orass 1089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
23		df-or 848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏𝑆𝑑 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
24	22, 23	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏𝑆𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) ↔ (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
25	21, 24	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → (¬ 𝑏𝑆𝑑 → (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))
26	25	orim2d 968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑) → (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))))
27	20, 26	im2anan9 620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((¬ 𝑎𝑅𝑐 ∧ (¬ 𝑎 = 𝑐 ∨ ¬ 𝑏𝑆𝑑)) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)))))
28		pm2.53 851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → 𝑐𝑅𝑎))
29		orc 867	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐𝑅𝑎 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
30	28, 29	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
31	30	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑎 = 𝑐 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
32		orel1 888	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑏 = 𝑑 → ((𝑏 = 𝑑 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
33	32	orim2d 968	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑏 = 𝑑 → ((¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏)) → (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)))
34	33	anim2d 612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑏 = 𝑑 → (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))))
35		imor 853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 → 𝑑𝑆𝑏) ↔ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏))
36	35	biimpri 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑎 = 𝑐 → 𝑑𝑆𝑏))
37	36	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → 𝑑𝑆𝑏))
38		equcomi 2016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → 𝑐 = 𝑎)
39	38	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))
40	39	olcd 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑐 ∧ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
41	40	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑐 → (𝑑𝑆𝑏 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
42	37, 41	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑐 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
43	29	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐𝑅𝑎 → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
44	42, 43	jaoi 857	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) → ((¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
45	44	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ 𝑑𝑆𝑏)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏)))
46	34, 45	syl6com 37	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 = 𝑐 ∨ 𝑐𝑅𝑎) ∧ (¬ 𝑎 = 𝑐 ∨ (𝑏 = 𝑑 ∨ 𝑑𝑆𝑏))) → (¬ 𝑏 = 𝑑 → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
47	31, 46	jaod 859	. . . . . . . . . . . . . . . . . . . . . 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 1087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
52		df-or 848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
53	51, 52	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))) ↔ (¬ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑)) → (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
54	50, 53	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ (𝑆 Or 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))
55		pm3.2 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))))
56	55	ad2ant2l 746	. . . . . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
68	67	an4s 660	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∨ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ∨ (((𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑐𝑅𝑎 ∨ (𝑐 = 𝑎 ∧ 𝑑𝑆𝑏))))))
69		breq12 5124	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
70		eqeq12 2752	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡 = 𝑢 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
71		breq12 5124	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
72	71	ancoms 458	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑢𝑇𝑡 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
73	69, 70, 72	3orbi123d 1437	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → ((𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∨ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ∨ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
74	3	xporderlem 8124	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
75		vex 3463	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ V
76		vex 3463	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
77	75, 76	opth 5451	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
78	3	xporderlem 8124	. . . . . . . . . . . . . . . . 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 660	. . . . . . . . . 10 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
86	85	expcom 413	. . . . . . . . 9 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
87	86	exlimivv 1932	. . . . . . . 8 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
88	87	com12 32	. . . . . . 7 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
89	88	exlimivv 1932	. . . . . 6 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))))
90	89	imp 406	. . . . 5 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
91	6, 7, 90	syl2anb 598	. . . 4 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
92	91	com12 32	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡)))
93	92	ralrimivv 3185	. 2 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)(𝑡𝑇𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢𝑇𝑡))
94		df-so 5562	. 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 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∀wral 3051 ⟨cop 4607 class class class wbr 5119 {copab 5181 Po wpo 5559 Or wor 5560 × cxp 5652 ‘cfv 6530 1^st c1st 7984 2^nd c2nd 7985

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402 ax-un 7727

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-po 5561 df-so 5562 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-iota 6483 df-fun 6532 df-fv 6538 df-1st 7986 df-2nd 7987

This theorem is referenced by: wexp 8127 rrx2plordso 48652

W3C validator