Metamath Proof Explorer


Theorem unfiOLD

Description: Obsolete version of unfi as of 7-Aug-2024. (Contributed by NM, 16-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion unfiOLD
|- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Proof

Step Hyp Ref Expression
1 diffi
 |-  ( B e. Fin -> ( B \ A ) e. Fin )
2 reeanv
 |-  ( E. x e. _om E. y e. _om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( E. x e. _om A ~~ x /\ E. y e. _om ( B \ A ) ~~ y ) )
3 isfi
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
4 isfi
 |-  ( ( B \ A ) e. Fin <-> E. y e. _om ( B \ A ) ~~ y )
5 3 4 anbi12i
 |-  ( ( A e. Fin /\ ( B \ A ) e. Fin ) <-> ( E. x e. _om A ~~ x /\ E. y e. _om ( B \ A ) ~~ y ) )
6 2 5 bitr4i
 |-  ( E. x e. _om E. y e. _om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7 nnacl
 |-  ( ( x e. _om /\ y e. _om ) -> ( x +o y ) e. _om )
8 unfilem3
 |-  ( ( x e. _om /\ y e. _om ) -> y ~~ ( ( x +o y ) \ x ) )
9 entr
 |-  ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10 9 expcom
 |-  ( y ~~ ( ( x +o y ) \ x ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
11 8 10 syl
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
12 disjdif
 |-  ( A i^i ( B \ A ) ) = (/)
13 disjdif
 |-  ( x i^i ( ( x +o y ) \ x ) ) = (/)
14 unen
 |-  ( ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) /\ ( ( A i^i ( B \ A ) ) = (/) /\ ( x i^i ( ( x +o y ) \ x ) ) = (/) ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
15 12 13 14 mpanr12
 |-  ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16 undif2
 |-  ( A u. ( B \ A ) ) = ( A u. B )
17 16 a1i
 |-  ( ( x e. _om /\ y e. _om ) -> ( A u. ( B \ A ) ) = ( A u. B ) )
18 nnaword1
 |-  ( ( x e. _om /\ y e. _om ) -> x C_ ( x +o y ) )
19 undif
 |-  ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20 18 19 sylib
 |-  ( ( x e. _om /\ y e. _om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21 17 20 breq12d
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) <-> ( A u. B ) ~~ ( x +o y ) ) )
22 15 21 syl5ib
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. B ) ~~ ( x +o y ) ) )
23 11 22 sylan2d
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24 breq2
 |-  ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25 24 rspcev
 |-  ( ( ( x +o y ) e. _om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. _om ( A u. B ) ~~ z )
26 isfi
 |-  ( ( A u. B ) e. Fin <-> E. z e. _om ( A u. B ) ~~ z )
27 25 26 sylibr
 |-  ( ( ( x +o y ) e. _om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28 7 23 27 syl6an
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29 28 rexlimivv
 |-  ( E. x e. _om E. y e. _om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30 6 29 sylbir
 |-  ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31 1 30 sylan2
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )