Theorem unxpdomlem3 9225

Description: Lemma for unxpdom 9226. (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 9222	. . 3 ⊢ (𝑎 ∈ V → (1o ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛))
2	1	elv 3462	. 2 ⊢ (1o ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛)
3		1sdom 9222	. . 3 ⊢ (𝑏 ∈ V → (1o ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
4	3	elv 3462	. 2 ⊢ (1o ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡)
5		reeanv 3239	. . 3 ⊢ (∃𝑚 ∈ 𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) ↔ (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
6		reeanv 3239	. . . . 5 ⊢ (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ↔ (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡))
7		vex 3461	. . . . . . . . 9 ⊢ 𝑎 ∈ V
8		vex 3461	. . . . . . . . 9 ⊢ 𝑏 ∈ V
9	7, 8	unex 7752	. . . . . . . 8 ⊢ (𝑎 ∪ 𝑏) ∈ V
10	7, 8	xpex 7758	. . . . . . . 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 4536	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏)
16	15	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏)
17	12, 16	opelxpd 5702	. . . . . . . . . . . 12 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩ ∈ (𝑎 × 𝑏))
18		simp2l 1218	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑛 ∈ 𝑎)
19		simp1l 1216	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑚 ∈ 𝑎)
20	18, 19	ifcld 4536	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎)
21	20	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎)
22		elun 4107	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑎 ∪ 𝑏) ↔ (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏))
23	22	bilani 510	. . . . . . . . . . . . . 14 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏))
24	23	orcanai 1018	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑏)
25	21, 24	opelxpd 5702	. . . . . . . . . . . 12 ⊢ (((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩ ∈ (𝑎 × 𝑏))
26	17, 25	ifclda 4525	. . . . . . . . . . 11 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩) ∈ (𝑎 × 𝑏))
27	11, 26	eqeltrid 2869	. . . . . . . . . 10 ⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → 𝐺 ∈ (𝑎 × 𝑏))
28		unxpdomlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)
29	27, 28	fmptd 7113	. . . . . . . . 9 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏))
30	28, 11	unxpdomlem1 9223	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
31	30	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
32		iftrue 4495	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
33	32	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
34	31, 33	sylan9eq 2820	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩)
35	28, 11	unxpdomlem1 9223	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
36	35	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
37		iftrue 4495	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
38	37	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
39	36, 38	sylan9eq 2820	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩)
40	34, 39	eqeq12d 2781	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩ = ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩))
41		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
42		vex 3461	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
43		vex 3461	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
44	42, 43	ifex 4540	. . . . . . . . . . . . . 14 ⊢ if(𝑧 = 𝑚, 𝑡, 𝑠) ∈ V
45	41, 44	opth1 5459	. . . . . . . . . . . . 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 9224	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
51	50	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
52		eqcom 2772	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑤) = (𝐹‘𝑧))
53		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑧 ∈ (𝑎 ∪ 𝑏))
54	28, 11, 53, 48, 49	unxpdomlem2 9224	. . . . . . . . . . . . . . 15 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑤 ∈ 𝑎 ∧ ¬ 𝑧 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧))
55	54	ancom2s 663	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧))
56	55	pm2.21d 122	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑧 = 𝑤))
57	52, 56	biimtrid 245	. . . . . . . . . . . 12 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
58		iffalse 4498	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
59	58	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
60	31, 59	sylan9eq 2820	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)
61		iffalse 4498	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
62	61	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, ⟨𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
63	36, 62	sylan9eq 2820	. . . . . . . . . . . . . 14 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩)
64	60, 63	eqeq12d 2781	. . . . . . . . . . . . 13 ⊢ ((((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩ = ⟨if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤⟩))
65		vex 3461	. . . . . . . . . . . . . . . 16 ⊢ 𝑛 ∈ V
66		vex 3461	. . . . . . . . . . . . . . . 16 ⊢ 𝑚 ∈ V
67	65, 66	ifex 4540	. . . . . . . . . . . . . . 15 ⊢ if(𝑧 = 𝑡, 𝑛, 𝑚) ∈ V
68	67, 41	opth 5460	. . . . . . . . . . . . . 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 3210	. . . . . . . . . 10 ⊢ ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
73	72	3ad2ant3 1153	. . . . . . . . 9 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
74		dff13 7257	. . . . . . . . 9 ⊢ (𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏) ↔ (𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏) ∧ ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
75	29, 73, 74	sylanbrc 595	. . . . . . . 8 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏))
76		f1dom2g 8972	. . . . . . . 8 ⊢ (((𝑎 ∪ 𝑏) ∈ V ∧ (𝑎 × 𝑏) ∈ V ∧ 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
77	9, 10, 75, 76	mp3an12i 1494	. . . . . . 7 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
78	77	3expia 1139	. . . . . 6 ⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏)) → ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
79	78	rexlimdvva 3224	. . . . 5 ⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
80	6, 79	biimtrrid 246	. . . 4 ⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → ((∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)))
81	80	rexlimivv 3209	. . 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 2146  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ∪ cun 3904  ifcif 4489  ⟨cop 4597   class class class wbr 5111   ↦ cmpt 5194   × cxp 5661  ⟶wf 6536  –1-1→wf1 6537  ‘cfv 6540  1_oc1o 8452   ≼ cdom 8947   ≺ csdm 8948

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-1o 8459  df-2o 8460  df-en 8950  df-dom 8951  df-sdom 8952

This theorem is used by:  unxpdom  9226