Theorem unxpdomlem3 9158

Description: Lemma for unxpdom 9159. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)

Hypotheses

Ref	Expression
unxpdomlem1.1	⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)
unxpdomlem1.2	⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)

Assertion

Ref	Expression
unxpdomlem3	⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))

Distinct variable group:   𝑎,𝑏,𝑚,𝑛,𝑠,𝑡,𝑥

Allowed substitution hints:   𝐹(𝑥,𝑡,𝑚,𝑛,𝑠,𝑎,𝑏)   𝐺(𝑥,𝑡,𝑚,𝑛,𝑠,𝑎,𝑏)

Proof of Theorem unxpdomlem3

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1sdom 9155	. . 3 ⊢ (𝑎 ∈ V → (1o ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛))
2	1	elv 3436	. 2 ⊢ (1o ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛)
3		1sdom 9155	. . 3 ⊢ (𝑏 ∈ V → (1o ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
4	3	elv 3436	. 2 ⊢ (1o ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡)
5		reeanv 3211	. . 3 ⊢ (∃𝑚 ∈ 𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) ↔ (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
6		reeanv 3211	. . . . 5 ⊢ (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ↔ (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
7		vex 3435	. . . . . . . . 9 ⊢ 𝑎 ∈ V
8		vex 3435	. . . . . . . . 9 ⊢ 𝑏 ∈ V
9	7, 8	unex 7687	. . . . . . . 8 ⊢ (𝑎 ∪ 𝑏) ∈ V
10	7, 8	xpex 7696	. . . . . . . 8 ⊢ (𝑎 × 𝑏) ∈ V
11		unxpdomlem1.2	. . . . . . . . . . 11 ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)
12		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑎)
13		simp2r 1207	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑡 ∈ 𝑏)
14		simp1r 1205	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑠 ∈ 𝑏)
15	13, 14	ifcld 4501	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏)
16	15	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏)
17	12, 16	opelxpd 5657	. . . . . . . . . . . 12 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩ ∈ (𝑎 × 𝑏))
18		simp2l 1206	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑛 ∈ 𝑎)
19		simp1l 1204	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑚 ∈ 𝑎)
20	18, 19	ifcld 4501	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎)
21	20	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎)
22		elun 4083	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑎 ∪ 𝑏) ↔ (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏))
23	22	bilani 505	. . . . . . . . . . . . . 14 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏))
24	23	orcanai 1010	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑏)
25	21, 24	opelxpd 5657	. . . . . . . . . . . 12 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩ ∈ (𝑎 × 𝑏))
26	17, 25	ifclda 4490	. . . . . . . . . . 11 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩) ∈ (𝑎 × 𝑏))
27	11, 26	eqeltrid 2843	. . . . . . . . . 10 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → 𝐺 ∈ (𝑎 × 𝑏))
28		unxpdomlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)
29	27, 28	fmptd 7055	. . . . . . . . 9 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏))
30	28, 11	unxpdomlem1 9156	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
31	30	ad2antrl 734	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
32		iftrue 4460	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
33	32	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
34	31, 33	sylan9eq 2794	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
35	28, 11	unxpdomlem1 9156	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
36	35	ad2antll 735	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
37		iftrue 4460	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
38	37	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
39	36, 38	sylan9eq 2794	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
40	34, 39	eqeq12d 2755	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩ = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩))
41		vex 3435	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
42		vex 3435	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
43		vex 3435	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
44	42, 43	ifex 4505	. . . . . . . . . . . . . 14 ⊢ if(𝑧 = 𝑚, 𝑡, 𝑠) ∈ V
45	41, 44	opth1 5415	. . . . . . . . . . . . 13 ⊢ (⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩ = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩ → 𝑧 = 𝑤)
46	40, 45	biimtrdi 254	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
47		simprr 778	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑤 ∈ (𝑎 ∪ 𝑏))
48		simpll 772	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ¬ 𝑚 = 𝑛)
49		simplr 774	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ¬ 𝑠 = 𝑡)
50	28, 11, 47, 48, 49	unxpdomlem2 9157	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
51	50	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
52		eqcom 2746	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑤) = (𝐹‘𝑧))
53		simprl 776	. . . . . . . . . . . . . . . 16 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑧 ∈ (𝑎 ∪ 𝑏))
54	28, 11, 53, 48, 49	unxpdomlem2 9157	. . . . . . . . . . . . . . 15 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑤 ∈ 𝑎 ∧ ¬ 𝑧 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧))
55	54	ancom2s 656	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧))
56	55	pm2.21d 121	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑧 = 𝑤))
57	52, 56	biimtrid 243	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
58		iffalse 4463	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
59	58	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
60	31, 59	sylan9eq 2794	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
61		iffalse 4463	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
62	61	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
63	36, 62	sylan9eq 2794	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
64	60, 63	eqeq12d 2755	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
65		vex 3435	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
66		vex 3435	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
67	65, 66	ifex 4505	. . . . . . . . . . . . . . 15 ⊢ if(𝑧 = 𝑡, 𝑛, 𝑚) ∈ V
68	67, 41	opth 5416	. . . . . . . . . . . . . 14 ⊢ (⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩ ↔ (if(𝑧 = 𝑡, 𝑛, 𝑚) = if(𝑤 = 𝑡, 𝑛, 𝑚) ∧ 𝑧 = 𝑤))
69	68	simprbi 498	. . . . . . . . . . . . 13 ⊢ (⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩ → 𝑧 = 𝑤)
70	64, 69	biimtrdi 254	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
71	46, 51, 57, 70	4casesdan 1047	. . . . . . . . . . 11 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
72	71	ralrimivva 3182	. . . . . . . . . 10 ⊢ ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
73	72	3ad2ant3 1141	. . . . . . . . 9 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
74		dff13 7198	. . . . . . . . 9 ⊢ (𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏) ↔ (𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏) ∧ ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
75	29, 73, 74	sylanbrc 589	. . . . . . . 8 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏))
76		f1dom2g 8906	. . . . . . . 8 ⊢ (((𝑎 ∪ 𝑏) ∈ V ∧ (𝑎 × 𝑏) ∈ V ∧ 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
77	9, 10, 75, 76	mp3an12i 1473	. . . . . . 7 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
78	77	3expia 1127	. . . . . 6 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏)) → ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
79	78	rexlimdvva 3196	. . . . 5 ⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
80	6, 79	biimtrrid 244	. . . 4 ⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → ((∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
81	80	rexlimivv 3181	. . 3 ⊢ (∃𝑚 ∈ 𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
82	5, 81	sylbir 236	. 2 ⊢ ((∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
83	2, 4, 82	syl2anb 604	1 ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  Vcvv 3431   ∪ cun 3881  ifcif 4454  ⟨cop 4561   class class class wbr 5072   ↦ cmpt 5153   × cxp 5616  ⟶wf 6481  –1-1→wf1 6482  ‘cfv 6485  1_oc1o 8388   ≼ cdom 8881   ≺ csdm 8882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-1o 8395  df-2o 8396  df-en 8884  df-dom 8885  df-sdom 8886

This theorem is referenced by:  unxpdom  9159