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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴𝐵 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 diffi ( 𝐵 ∈ Fin → ( 𝐵𝐴 ) ∈ Fin )
2 reeanv ( ∃ 𝑥 ∈ ω ∃ 𝑦 ∈ ω ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ω 𝐴𝑥 ∧ ∃ 𝑦 ∈ ω ( 𝐵𝐴 ) ≈ 𝑦 ) )
3 isfi ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴𝑥 )
4 isfi ( ( 𝐵𝐴 ) ∈ Fin ↔ ∃ 𝑦 ∈ ω ( 𝐵𝐴 ) ≈ 𝑦 )
5 3 4 anbi12i ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴 ) ∈ Fin ) ↔ ( ∃ 𝑥 ∈ ω 𝐴𝑥 ∧ ∃ 𝑦 ∈ ω ( 𝐵𝐴 ) ≈ 𝑦 ) )
6 2 5 bitr4i ( ∃ 𝑥 ∈ ω ∃ 𝑦 ∈ ω ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ 𝑦 ) ↔ ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴 ) ∈ Fin ) )
7 nnacl ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 +o 𝑦 ) ∈ ω )
8 unfilem3 ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → 𝑦 ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) )
9 entr ( ( ( 𝐵𝐴 ) ≈ 𝑦𝑦 ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) → ( 𝐵𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) )
10 9 expcom ( 𝑦 ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) → ( ( 𝐵𝐴 ) ≈ 𝑦 → ( 𝐵𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
11 8 10 syl ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐵𝐴 ) ≈ 𝑦 → ( 𝐵𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
12 disjdif ( 𝐴 ∩ ( 𝐵𝐴 ) ) = ∅
13 disjdif ( 𝑥 ∩ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ∅
14 unen ( ( ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) ∧ ( ( 𝐴 ∩ ( 𝐵𝐴 ) ) = ∅ ∧ ( 𝑥 ∩ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ∅ ) ) → ( 𝐴 ∪ ( 𝐵𝐴 ) ) ≈ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
15 12 13 14 mpanr12 ( ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) → ( 𝐴 ∪ ( 𝐵𝐴 ) ) ≈ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) )
16 undif2 ( 𝐴 ∪ ( 𝐵𝐴 ) ) = ( 𝐴𝐵 )
17 16 a1i ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ∪ ( 𝐵𝐴 ) ) = ( 𝐴𝐵 ) )
18 nnaword1 ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → 𝑥 ⊆ ( 𝑥 +o 𝑦 ) )
19 undif ( 𝑥 ⊆ ( 𝑥 +o 𝑦 ) ↔ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ( 𝑥 +o 𝑦 ) )
20 18 19 sylib ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) = ( 𝑥 +o 𝑦 ) )
21 17 20 breq12d ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ∪ ( 𝐵𝐴 ) ) ≈ ( 𝑥 ∪ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) ↔ ( 𝐴𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
22 15 21 syl5ib ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ ( ( 𝑥 +o 𝑦 ) ∖ 𝑥 ) ) → ( 𝐴𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
23 11 22 sylan2d ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ 𝑦 ) → ( 𝐴𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
24 breq2 ( 𝑧 = ( 𝑥 +o 𝑦 ) → ( ( 𝐴𝐵 ) ≈ 𝑧 ↔ ( 𝐴𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) )
25 24 rspcev ( ( ( 𝑥 +o 𝑦 ) ∈ ω ∧ ( 𝐴𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) → ∃ 𝑧 ∈ ω ( 𝐴𝐵 ) ≈ 𝑧 )
26 isfi ( ( 𝐴𝐵 ) ∈ Fin ↔ ∃ 𝑧 ∈ ω ( 𝐴𝐵 ) ≈ 𝑧 )
27 25 26 sylibr ( ( ( 𝑥 +o 𝑦 ) ∈ ω ∧ ( 𝐴𝐵 ) ≈ ( 𝑥 +o 𝑦 ) ) → ( 𝐴𝐵 ) ∈ Fin )
28 7 23 27 syl6an ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ 𝑦 ) → ( 𝐴𝐵 ) ∈ Fin ) )
29 28 rexlimivv ( ∃ 𝑥 ∈ ω ∃ 𝑦 ∈ ω ( 𝐴𝑥 ∧ ( 𝐵𝐴 ) ≈ 𝑦 ) → ( 𝐴𝐵 ) ∈ Fin )
30 6 29 sylbir ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴 ) ∈ Fin ) → ( 𝐴𝐵 ) ∈ Fin )
31 1 30 sylan2 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴𝐵 ) ∈ Fin )