Theorem unfilem3 4539

Description: Lemma for proving that the union of two finite sets is finite.

Assertion

Ref	Expression
unfilem3	|- ((A e. om /\ B e. om) -> B ~~ ((A +o B) \ A))

Proof of Theorem unfilem3

Step	Hyp	Ref	Expression
1		f1oeq1 3681	. . . 4 |- (f = {<.x, y>. | (x e. B /\ y = (A +o x))} -> (f:B-1-1-onto->((A +o B) \ A) <-> {<.x, y>. | (x e. B /\ y = (A +o x))}:B-1-1-onto->((A +o B) \ A)))
2	1	cla4egv 1861	. . 3 |- ({<.x, y>. | (x e. B /\ y = (A +o x))} e. V -> ({<.x, y>. | (x e. B /\ y = (A +o x))}:B-1-1-onto->((A +o B) \ A) -> E.f f:B-1-1-onto->((A +o B) \ A)))
3		opreq1 3965	. . . . . . . . . . 11 |- (A = if(A e. om, A, (/)) -> (A +o x) = (if(A e. om, A, (/)) +o x))
4	3	eqeq2d 1485	. . . . . . . . . 10 |- (A = if(A e. om, A, (/)) -> (y = (A +o x) <-> y = (if(A e. om, A, (/)) +o x)))
5	4	anbi2d 615	. . . . . . . . 9 |- (A = if(A e. om, A, (/)) -> ((x e. B /\ y = (A +o x)) <-> (x e. B /\ y = (if(A e. om, A, (/)) +o x))))
6	5	opabbidv 2667	. . . . . . . 8 |- (A = if(A e. om, A, (/)) -> {<.x, y>. | (x e. B /\ y = (A +o x))} = {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))})
7		f1oeq1 3681	. . . . . . . 8 |- ({<.x, y>. | (x e. B /\ y = (A +o x))} = {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))} -> ({<.x, y>. | (x e. B /\ y = (A +o x))}:B-1-1-onto->((A +o B) \ A) <-> {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((A +o B) \ A)))
8	6, 7	syl 10	. . . . . . 7 |- (A = if(A e. om, A, (/)) -> ({<.x, y>. | (x e. B /\ y = (A +o x))}:B-1-1-onto->((A +o B) \ A) <-> {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((A +o B) \ A)))
9		opreq1 3965	. . . . . . . . . 10 |- (A = if(A e. om, A, (/)) -> (A +o B) = (if(A e. om, A, (/)) +o B))
10	9	difeq1d 2156	. . . . . . . . 9 |- (A = if(A e. om, A, (/)) -> ((A +o B) \ A) = ((if(A e. om, A, (/)) +o B) \ A))
11		difeq2 2152	. . . . . . . . 9 |- (A = if(A e. om, A, (/)) -> ((if(A e. om, A, (/)) +o B) \ A) = ((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))))
12	10, 11	eqtrd 1506	. . . . . . . 8 |- (A = if(A e. om, A, (/)) -> ((A +o B) \ A) = ((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))))
13		f1oeq3 3683	. . . . . . . 8 |- (((A +o B) \ A) = ((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))) -> ({<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((A +o B) \ A) <-> {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/)))))
14	12, 13	syl 10	. . . . . . 7 |- (A = if(A e. om, A, (/)) -> ({<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((A +o B) \ A) <-> {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/)))))
15	8, 14	bitrd 527	. . . . . 6 |- (A = if(A e. om, A, (/)) -> ({<.x, y>. | (x e. B /\ y = (A +o x))}:B-1-1-onto->((A +o B) \ A) <-> {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/)))))
16		eleq2 1534	. . . . . . . . . 10 |- (B = if(B e. om, B, (/)) -> (x e. B <-> x e. if(B e. om, B, (/))))
17	16	anbi1d 616	. . . . . . . . 9 |- (B = if(B e. om, B, (/)) -> ((x e. B /\ y = (if(A e. om, A, (/)) +o x)) <-> (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))))
18	17	opabbidv 2667	. . . . . . . 8 |- (B = if(B e. om, B, (/)) -> {<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))} = {<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))})
19		f1oeq1 3681	. . . . . . . 8 |- ({<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))} = {<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))} -> ({<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))) <-> {<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/)))))
20	18, 19	syl 10	. . . . . . 7 |- (B = if(B e. om, B, (/)) -> ({<.x, y>. | (x e. B /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))) <-> {<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/)))))
21		f1oeq2 3682	. . . . . . 7 |- (B = if(B e. om, B, (/)) -> ({<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))}:B-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))) <-> {<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))}:if(B e. om, B, (/))-1-1-onto->((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/)))))
22		opreq2 3966	. . . . . . . . 9 |- (B = if(B e. om, B, (/)) -> (if(A e. om, A, (/)) +o B) = (if(A e. om, A, (/)) +o if(B e. om, B, (/))))
23	22	difeq1d 2156	. . . . . . . 8 |- (B = if(B e. om, B, (/)) -> ((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))) = ((if(A e. om, A, (/)) +o if(B e. om, B, (/))) \ if(A e. om, A, (/))))
24		f1oeq3 3683	. . . . . . . 8 |- (((if(A e. om, A, (/)) +o B) \ if(A e. om, A, (/))) = ((if(A e. om, A, (/)) +o if(B e. om, B, (/))) \ if(A e. om, A, (/))) -> ({<.x, y>. | (x e. if(B e. om, B, (/)) /\ y = (if(A e. om, A, (/)) +o x))}:if(B e. om,