Theorem unxpdomlem 4854

Description: Lemma for unxpdom 4855.

Hypotheses

Ref	Expression
unxpdomlem.1	⊢ A ∈ V
unxpdomlem.2	⊢ B ∈ V

Assertion

Ref	Expression
unxpdomlem	⊢ ((1o ≺ A ⋀ 1o ≺ B) → (A ∪ B) ≼ (A × B))

Proof of Theorem unxpdomlem

Step	Hyp	Ref	Expression
1		eqeq1 1484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = f → (x = w ↔ f = w))
2	1	ifbid 2376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = f → if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, x)))
3		ifeq2 2369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = f → if(y = v, v, x) = if(y = v, v, f))
4	3	ifeq2d 2374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = f → if(f = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, f)))
5	2, 4	eqtrd 1510	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = f → if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(f = w, if(y = v, w, y), if(y = v, v, f)))
6	5	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 ⊢ (x = f → ( if(x = w, if(y = v, w, y), if(y = v, v, x)) = f ↔ if(f = w, if(y = v, w, y), if(y = v, v, f)) = f))
7		ifeq12 2372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( if(y = v, w, y) = if(v = v, w, v) ⋀ if(y = v, v, f) = if(v = v, v, f)) → if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(v = v, w, v), if(v = v, v, f)))
8		eqeq1 1484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = v → (y = v ↔ v = v))
9	8	ifbid 2376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = v → if(y = v, w, y) = if(v = v, w, y))
10		ifeq2 2369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = v → if(v = v, w, y) = if(v = v, w, v))
11	9, 10	eqtrd 1510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = v → if(y = v, w, y) = if(v = v, w, v))
12	8	ifbid 2376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = v → if(y = v, v, f) = if(v = v, v, f))
13	7, 11, 12	sylanc 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = v → if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(v = v, w, v), if(v = v, v, f)))
14	13	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 ⊢ (y = v → ( if(f = w, if(y = v, w, y), if(y = v, v, f)) = f ↔ if(f = w, if(v = v, w, v), if(v = v, v, f)) = f))
15	6, 14	rcla42ev 1884	. . . . . . . . . . . . . . . . 17 ⊢ ((f ∈ A ⋀ v ∈ B ⋀ if(f = w, if(v = v, w, v), if(v = v, v, f)) = f) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
16		eqid 1478	. . . . . . . . . . . . . . . . . . 19 ⊢ v = v
17		iftrue 2370	. . . . . . . . . . . . . . . . . . 19 ⊢ (v = v → if(v = v, w, v) = w)
18	16, 17	ax-mp 7	. . . . . . . . . . . . . . . . . 18 ⊢ if(v = v, w, v) = w
19		iftrue 2370	. . . . . . . . . . . . . . . . . 18 ⊢ (f = w → if(f = w, if(v = v, w, v), if(v = v, v, f)) = if(v = v, w, v))
20		id 59	. . . . . . . . . . . . . . . . . 18 ⊢ (f = w → f = w)
21	18, 19, 20	3eqtr4a 1535	. . . . . . . . . . . . . . . . 17 ⊢ (f = w → if(f = w, if(v = v, w, v), if(v = v, v, f)) = f)
22	15, 21	syl3an3 863	. . . . . . . . . . . . . . . 16 ⊢ ((f ∈ A ⋀ v ∈ B ⋀ f = w) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
23	22	3exp 834	. . . . . . . . . . . . . . 15 ⊢ (f ∈ A → (v ∈ B → (f = w → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
24	23	com3l 34	. . . . . . . . . . . . . 14 ⊢ (v ∈ B → (f = w → (f ∈ A → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
25	24	ad2antlr 407	. . . . . . . . . . . . 13 ⊢ (((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v) → (f = w → (f ∈ A → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
26		ifeq12 2372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( if(y = v, w, y) = if(t = v, w, t) ⋀ if(y = v, v, f) = if(t = v, v, f)) → if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(t = v, w, t), if(t = v, v, f)))
27		eqeq1 1484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y = t → (y = v ↔ t = v))
28	27	ifbid 2376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = t → if(y = v, w, y) = if(t = v, w, y))
29		ifeq2 2369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = t → if(t = v, w, y) = if(t = v, w, t))
30	28, 29	eqtrd 1510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = t → if(y = v, w, y) = if(t = v, w, t))
31	27	ifbid 2376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = t → if(y = v, v, f) = if(t = v, v, f))
32	26, 30, 31	sylanc 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = t → if(f = w, if(y = v, w, y), if(y = v, v, f)) = if(f = w, if(t = v, w, t), if(t = v, v, f)))
33	32	eqeq1d 1486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = t → ( if(f = w, if(y = v, w, y), if(y = v, v, f)) = f ↔ if(f = w, if(t = v, w, t), if(t = v, v, f)) = f))
34	6, 33	rcla42ev 1884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f ∈ A ⋀ t ∈ B ⋀ if(f = w, if(t = v, w, t), if(t = v, v, f)) = f) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
35		iffalse 2371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ f = w → if(f = w, if(t = v, w, t), if(t = v, v, f)) = if(t = v, v, f))
36		iffalse 2371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ t = v → if(t = v, v, f) = f)
37	35, 36	sylan9eqr 1532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ t = v ⋀ ¬ f = w) → if(f = w, if(t = v, w, t), if(t = v, v, f)) = f)
38	34, 37	syl3an3 863	. . . . . . . . . . . . . . . . . 18 ⊢ ((f ∈ A ⋀ t ∈ B ⋀ (¬ t = v ⋀ ¬ f = w)) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
39	38	3exp 834	. . . . . . . . . . . . . . . . 17 ⊢ (f ∈ A → (t ∈ B → ((¬ t = v ⋀ ¬ f = w) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
40	39	exp4a 380	. . . . . . . . . . . . . . . 16 ⊢ (f ∈ A → (t ∈ B → (¬ t = v → (¬ f = w → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))))
41	40	imp3a 361	. . . . . . . . . . . . . . 15 ⊢ (f ∈ A → ((t ∈ B ⋀ ¬ t = v) → (¬ f = w → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
42	41	com3l 34	. . . . . . . . . . . . . 14 ⊢ ((t ∈ B ⋀ ¬ t = v) → (¬ f = w → (f ∈ A → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
43	42	adantlr 395	. . . . . . . . . . . . 13 ⊢ (((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v) → (¬ f = w → (f ∈ A → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
44	25, 43	pm2.61d 127	. . . . . . . . . . . 12 ⊢ (((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v) → (f ∈ A → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))
45	44	adantl 390	. . . . . . . . . . 11 ⊢ ((((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) ⋀ ((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v)) → (f ∈ A → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))
46		eqeq1 1484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = u → (x = w ↔ u = w))
47	46	ifbid 2376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = u → if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(u = w, if(y = v, w, y), if(y = v, v, x)))
48		ifeq2 2369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = u → if(y = v, v, x) = if(y = v, v, u))
49	48	ifeq2d 2374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = u → if(u = w, if(y = v, w, y), if(y = v, v, x)) = if(u = w, if(y = v, w, y), if(y = v, v, u)))
50	47, 49	eqtrd 1510	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = u → if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(u = w, if(y = v, w, y), if(y = v, v, u)))
51	50	eqeq1d 1486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = u → ( if(x = w, if(y = v, w, y), if(y = v, v, x)) = f ↔ if(u = w, if(y = v, w, y), if(y = v, v, u)) = f))
52		ifeq12 2372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( if(y = v, w, y) = if(f = v, w, f) ⋀ if(y = v, v, u) = if(f = v, v, u)) → if(u = w, if(y = v, w, y), if(y = v, v, u)) = if(u = w, if(f = v, w, f), if(f = v, v, u)))
53		eqeq1 1484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y = f → (y = v ↔ f = v))
54	53	ifbid 2376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = f → if(y = v, w, y) = if(f = v, w, y))
55		ifeq2 2369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = f → if(f = v, w, y) = if(f = v, w, f))
56	54, 55	eqtrd 1510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = f → if(y = v, w, y) = if(f = v, w, f))
57	53	ifbid 2376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = f → if(y = v, v, u) = if(f = v, v, u))
58	52, 56, 57	sylanc 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = f → if(u = w, if(y = v, w, y), if(y = v, v, u)) = if(u = w, if(f = v, w, f), if(f = v, v, u)))
59	58	eqeq1d 1486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = f → ( if(u = w, if(y = v, w, y), if(y = v, v, u)) = f ↔ if(u = w, if(f = v, w, f), if(f = v, v, u)) = f))
60	51, 59	rcla42ev 1884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((u ∈ A ⋀ f ∈ B ⋀ if(u = w, if(f = v, w, f), if(f = v, v, u)) = f) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
61		iffalse 2371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ u = w → if(u = w, if(f = v, w, f), if(f = v, v, u)) = if(f = v, v, u))
62		iftrue 2370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f = v → if(f = v, v, u) = v)
63		equcomi 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f = v → v = f)
64	62, 63	eqtrd 1510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f = v → if(f = v, v, u) = f)
65	61, 64	sylan9eqr 1532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f = v ⋀ ¬ u = w) → if(u = w, if(f = v, w, f), if(f = v, v, u)) = f)
66	60, 65	syl3an3 863	. . . . . . . . . . . . . . . . . 18 ⊢ ((u ∈ A ⋀ f ∈ B ⋀ (f = v ⋀ ¬ u = w)) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
67	66	3exp 834	. . . . . . . . . . . . . . . . 17 ⊢ (u ∈ A → (f ∈ B → ((f = v ⋀ ¬ u = w) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
68	67	exp4a 380	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ A → (f ∈ B → (f = v → (¬ u = w → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))))
69	68	com24 37	. . . . . . . . . . . . . . 15 ⊢ (u ∈ A → (¬ u = w → (f = v → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))))
70	69	imp 350	. . . . . . . . . . . . . 14 ⊢ ((u ∈ A ⋀ ¬ u = w) → (f = v → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
71	70	adantlr 395	. . . . . . . . . . . . 13 ⊢ (((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) → (f = v → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
72		eqeq1 1484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = w → (x = w ↔ w = w))
73	72	ifbid 2376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = w → if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(w = w, if(y = v, w, y), if(y = v, v, x)))
74		ifeq2 2369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = w → if(y = v, v, x) = if(y = v, v, w))
75	74	ifeq2d 2374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = w → if(w = w, if(y = v, w, y), if(y = v, v, x)) = if(w = w, if(y = v, w, y), if(y = v, v, w)))
76	73, 75	eqtrd 1510	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = w → if(x = w, if(y = v, w, y), if(y = v, v, x)) = if(w = w, if(y = v, w, y), if(y = v, v, w)))
77	76	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 ⊢ (x = w → ( if(x = w, if(y = v, w, y), if(y = v, v, x)) = f ↔ if(w = w, if(y = v, w, y), if(y = v, v, w)) = f))
78		ifeq12 2372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( if(y = v, w, y) = if(f = v, w, f) ⋀ if(y = v, v, w) = if(f = v, v, w)) → if(w = w, if(y = v, w, y), if(y = v, v, w)) = if(w = w, if(f = v, w, f), if(f = v, v, w)))
79	53	ifbid 2376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = f → if(y = v, v, w) = if(f = v, v, w))
80	78, 56, 79	sylanc 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = f → if(w = w, if(y = v, w, y), if(y = v, v, w)) = if(w = w, if(f = v, w, f), if(f = v, v, w)))
81	80	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 ⊢ (y = f → ( if(w = w, if(y = v, w, y), if(y = v, v, w)) = f ↔ if(w = w, if(f = v, w, f), if(f = v, v, w)) = f))
82	77, 81	rcla42ev 1884	. . . . . . . . . . . . . . . . 17 ⊢ ((w ∈ A ⋀ f ∈ B ⋀ if(w = w, if(f = v, w, f), if(f = v, v, w)) = f) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
83		iffalse 2371	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ f = v → if(f = v, w, f) = f)
84		eqid 1478	. . . . . . . . . . . . . . . . . . 19 ⊢ w = w
85		iftrue 2370	. . . . . . . . . . . . . . . . . . 19 ⊢ (w = w → if(w = w, if(f = v, w, f), if(f = v, v, w)) = if(f = v, w, f))
86	84, 85	ax-mp 7	. . . . . . . . . . . . . . . . . 18 ⊢ if(w = w, if(f = v, w, f), if(f = v, v, w)) = if(f = v, w, f)
87	83, 86	syl5eq 1522	. . . . . . . . . . . . . . . . 17 ⊢ (¬ f = v → if(w = w, if(f = v, w, f), if(f = v, v, w)) = f)
88	82, 87	syl3an3 863	. . . . . . . . . . . . . . . 16 ⊢ ((w ∈ A ⋀ f ∈ B ⋀ ¬ f = v) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)
89	88	3exp 834	. . . . . . . . . . . . . . 15 ⊢ (w ∈ A → (f ∈ B → (¬ f = v → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
90	89	com23 32	. . . . . . . . . . . . . 14 ⊢ (w ∈ A → (¬ f = v → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
91	90	ad2antlr 407	. . . . . . . . . . . . 13 ⊢ (((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) → (¬ f = v → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f)))
92	71, 91	pm2.61d 127	. . . . . . . . . . . 12 ⊢ (((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))
93	92	adantr 391	. . . . . . . . . . 11 ⊢ ((((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) ⋀ ((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v)) → (f ∈ B → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))
94	45, 93	jaod 426	. . . . . . . . . 10 ⊢ ((((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) ⋀ ((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v)) → ((f ∈ A ⋁ f ∈ B) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))
95		elun 2176	. . . . . . . . . 10 ⊢ (f ∈ (A ∪ B) ↔ (f ∈ A ⋁ f ∈ B))
96	94, 95	syl5ib 206	. . . . . . . . 9 ⊢ ((((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) ⋀ ((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v)) → (f ∈ (A ∪ B) → ∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f))
97		eqcom 1480	. . . . . . . . . . 11 ⊢ ( if(x = w, if(y = v, w, y), if(y = v, v, x)) = f ↔ f = if(x = w, if(y = v, w, y), if(y = v, v, x)))
98	97	2rexbii 1673	. . . . . . . . . 10 ⊢ (∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f ↔ ∃x ∈ A ∃y ∈ B f = if(x = w, if(y = v, w, y), if(y = v, v, x)))
99		visset 1816	. . . . . . . . . . . . 13 ⊢ w ∈ V
100		visset 1816	. . . . . . . . . . . . 13 ⊢ y ∈ V
101	99, 100	ifex 2404	. . . . . . . . . . . 12 ⊢ if(y = v, w, y) ∈ V
102		visset 1816	. . . . . . . . . . . . 13 ⊢ v ∈ V
103		visset 1816	. . . . . . . . . . . . 13 ⊢ x ∈ V
104	102, 103	ifex 2404	. . . . . . . . . . . 12 ⊢ if(y = v, v, x) ∈ V
105	101, 104	ifex 2404	. . . . . . . . . . 11 ⊢ if(x = w, if(y = v, w, y), if(y = v, v, x)) ∈ V
106		eqid 1478	. . . . . . . . . . 11 ⊢ {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = if(x = w, if(y = v, w, y), if(y = v, v, x)))} = {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = if(x = w, if(y = v, w, y), if(y = v, v, x)))}
107	105, 106	elrnoprab 4131	. . . . . . . . . 10 ⊢ (f ∈ ran {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = if(x = w, if(y = v, w, y), if(y = v, v, x)))} ↔ ∃x ∈ A ∃y ∈ B f = if(x = w, if(y = v, w, y), if(y = v, v, x)))
108	98, 107	bitr4 176	. . . . . . . . 9 ⊢ (∃x ∈ A ∃y ∈ B if(x = w, if(y = v, w, y), if(y = v, v, x)) = f ↔ f ∈ ran {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = if(x = w, if(y = v, w, y), if(y = v, v, x)))})
109	96, 108	syl6ib 212	. . . . . . . 8 ⊢ ((((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) ⋀ ((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v)) → (f ∈ (A ∪ B) → f ∈ ran {⟨⟨x, y⟩, z⟩∣((x ∈ A ⋀ y ∈ B) ⋀ z = if(x = w, if(y = v, w, y), if(y = v, v, x)))}))
110	109	ssrdv 2073	. . . . . . 7 ⊢ ((((u ∈ A ⋀ w ∈ A) ⋀ ¬ u = w) ⋀ ((t ∈ B ⋀ v ∈ B) ⋀ ¬ t = v)) → (A ∪ B) ⊆ ran {⟨⟨x, y⟩, z&