Theorem unxpdomlem3 9232

Description: Lemma for unxpdom 9233. (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 9229	. . 3 ⊢ (𝑎 ∈ V → (1o ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛))
2	1	elv 3458	. 2 ⊢ (1o ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛)
3		1sdom 9229	. . 3 ⊢ (𝑏 ∈ V → (1o ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
4	3	elv 3458	. 2 ⊢ (1o ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡)
5		reeanv 3236	. . 3 ⊢ (∃𝑚 ∈ 𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) ↔ (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
6		reeanv 3236	. . . . 5 ⊢ (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ↔ (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
7		vex 3457	. . . . . . . . 9 ⊢ 𝑎 ∈ V
8		vex 3457	. . . . . . . . 9 ⊢ 𝑏 ∈ V
9	7, 8	unex 7750	. . . . . . . 8 ⊢ (𝑎 ∪ 𝑏) ∈ V
10	7, 8	xpex 7756	. . . . . . . 8 ⊢ (𝑎 × 𝑏) ∈ V
11		unxpdomlem1.2	. . . . . . . . . . 11 ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)
12		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑎)
13		simp2r 1219	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑡 ∈ 𝑏)
14		simp1r 1217	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑠 ∈ 𝑏)
15	13, 14	ifcld 4532	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏)
16	15	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏)
17	12, 16	opelxpd 5698	. . . . . . . . . . . 12 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩ ∈ (𝑎 × 𝑏))
18		simp2l 1218	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑛 ∈ 𝑎)
19		simp1l 1216	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑚 ∈ 𝑎)
20	18, 19	ifcld 4532	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎)
21	20	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎)
22		elun 4103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑎 ∪ 𝑏) ↔ (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏))
23	22	bilani 510	. . . . . . . . . . . . . 14 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏))
24	23	orcanai 1018	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑏)
25	21, 24	opelxpd 5698	. . . . . . . . . . . 12 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩ ∈ (𝑎 × 𝑏))
26	17, 25	ifclda 4521	. . . . . . . . . . 11 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩) ∈ (𝑎 × 𝑏))
27	11, 26	eqeltrid 2866	. . . . . . . . . 10 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → 𝐺 ∈ (𝑎 × 𝑏))
28		unxpdomlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)
29	27, 28	fmptd 7111	. . . . . . . . 9 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏))
30	28, 11	unxpdomlem1 9230	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
31	30	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
32		iftrue 4491	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
33	32	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
34	31, 33	sylan9eq 2817	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
35	28, 11	unxpdomlem1 9230	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
36	35	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
37		iftrue 4491	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
38	37	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
39	36, 38	sylan9eq 2817	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
40	34, 39	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩ = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩))
41		vex 3457	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
42		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
43		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
44	42, 43	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if(𝑧 = 𝑚, 𝑡, 𝑠) ∈ V
45	41, 44	opth1 5455	. . . . . . . . . . . . 13 ⊢ (⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩ = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩ → 𝑧 = 𝑤)
46	40, 45	biimtrdi 256	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
47		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑤 ∈ (𝑎 ∪ 𝑏))
48		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ¬ 𝑚 = 𝑛)
49		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ¬ 𝑠 = 𝑡)
50	28, 11, 47, 48, 49	unxpdomlem2 9231	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
51	50	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
52		eqcom 2769	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑤) = (𝐹‘𝑧))
53		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑧 ∈ (𝑎 ∪ 𝑏))
54	28, 11, 53, 48, 49	unxpdomlem2 9231	. . . . . . . . . . . . . . 15 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑤 ∈ 𝑎 ∧ ¬ 𝑧 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧))
55	54	ancom2s 663	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧))
56	55	pm2.21d 122	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑧 = 𝑤))
57	52, 56	biimtrid 245	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
58		iffalse 4494	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
59	58	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
60	31, 59	sylan9eq 2817	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
61		iffalse 4494	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
62	61	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
63	36, 62	sylan9eq 2817	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
64	60, 63	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
65		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
66		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
67	65, 66	ifex 4536	. . . . . . . . . . . . . . 15 ⊢ if(𝑧 = 𝑡, 𝑛, 𝑚) ∈ V
68	67, 41	opth 5456	. . . . . . . . . . . . . 14 ⊢ (⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩ ↔ (if(𝑧 = 𝑡, 𝑛, 𝑚) = if(𝑤 = 𝑡, 𝑛, 𝑚) ∧ 𝑧 = 𝑤))
69	68	simprbi 503	. . . . . . . . . . . . 13 ⊢ (⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩ → 𝑧 = 𝑤)
70	64, 69	biimtrdi 256	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
71	46, 51, 57, 70	4casesdan 1057	. . . . . . . . . . 11 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
72	71	ralrimivva 3207	. . . . . . . . . 10 ⊢ ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
73	72	3ad2ant3 1153	. . . . . . . . 9 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
74		dff13 7255	. . . . . . . . 9 ⊢ (𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏) ↔ (𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏) ∧ ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
75	29, 73, 74	sylanbrc 595	. . . . . . . 8 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏))
76		f1dom2g 8979	. . . . . . . 8 ⊢ (((𝑎 ∪ 𝑏) ∈ V ∧ (𝑎 × 𝑏) ∈ V ∧ 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
77	9, 10, 75, 76	mp3an12i 1494	. . . . . . 7 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
78	77	3expia 1139	. . . . . 6 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏)) → ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
79	78	rexlimdvva 3221	. . . . 5 ⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
80	6, 79	biimtrrid 246	. . . 4 ⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → ((∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
81	80	rexlimivv 3206	. . 3 ⊢ (∃𝑚 ∈ 𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
82	5, 81	sylbir 238	. 2 ⊢ ((∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
83	2, 4, 82	syl2anb 610	1 ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ∪ cun 3900  ifcif 4485  ⟨cop 4593   class class class wbr 5107   ↦ cmpt 5190   × cxp 5657  ⟶wf 6533  –1-1→wf1 6534  ‘cfv 6537  1_oc1o 8452   ≼ cdom 8954   ≺ csdm 8955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-1o 8459  df-2o 8460  df-en 8957  df-dom 8958  df-sdom 8959

This theorem is used by:  unxpdom  9233