Metamath Proof Explorer


Theorem fin1a2lem12

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2lem12 ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) → ¬ 𝐵 ∈ FinIII )

Proof

Step Hyp Ref Expression
1 simpr ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → 𝐵 ∈ FinIII )
2 simpll1 ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → 𝐴 ⊆ 𝒫 𝐵 )
3 2 adantr ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑒 ∈ ω ) → 𝐴 ⊆ 𝒫 𝐵 )
4 ssrab2 { 𝑓𝐴𝑓𝑒 } ⊆ 𝐴
5 4 unissi { 𝑓𝐴𝑓𝑒 } ⊆ 𝐴
6 sspwuni ( 𝐴 ⊆ 𝒫 𝐵 𝐴𝐵 )
7 6 biimpi ( 𝐴 ⊆ 𝒫 𝐵 𝐴𝐵 )
8 5 7 sstrid ( 𝐴 ⊆ 𝒫 𝐵 { 𝑓𝐴𝑓𝑒 } ⊆ 𝐵 )
9 3 8 syl ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑒 ∈ ω ) → { 𝑓𝐴𝑓𝑒 } ⊆ 𝐵 )
10 elpw2g ( 𝐵 ∈ FinIII → ( { 𝑓𝐴𝑓𝑒 } ∈ 𝒫 𝐵 { 𝑓𝐴𝑓𝑒 } ⊆ 𝐵 ) )
11 10 ad2antlr ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑒 ∈ ω ) → ( { 𝑓𝐴𝑓𝑒 } ∈ 𝒫 𝐵 { 𝑓𝐴𝑓𝑒 } ⊆ 𝐵 ) )
12 9 11 mpbird ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑒 ∈ ω ) → { 𝑓𝐴𝑓𝑒 } ∈ 𝒫 𝐵 )
13 12 fmpttd ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) : ω ⟶ 𝒫 𝐵 )
14 vex 𝑑 ∈ V
15 14 sucex suc 𝑑 ∈ V
16 sssucid 𝑑 ⊆ suc 𝑑
17 ssdomg ( suc 𝑑 ∈ V → ( 𝑑 ⊆ suc 𝑑𝑑 ≼ suc 𝑑 ) )
18 15 16 17 mp2 𝑑 ≼ suc 𝑑
19 domtr ( ( 𝑓𝑑𝑑 ≼ suc 𝑑 ) → 𝑓 ≼ suc 𝑑 )
20 18 19 mpan2 ( 𝑓𝑑𝑓 ≼ suc 𝑑 )
21 20 a1i ( 𝑓𝐴 → ( 𝑓𝑑𝑓 ≼ suc 𝑑 ) )
22 21 ss2rabi { 𝑓𝐴𝑓𝑑 } ⊆ { 𝑓𝐴𝑓 ≼ suc 𝑑 }
23 uniss ( { 𝑓𝐴𝑓𝑑 } ⊆ { 𝑓𝐴𝑓 ≼ suc 𝑑 } → { 𝑓𝐴𝑓𝑑 } ⊆ { 𝑓𝐴𝑓 ≼ suc 𝑑 } )
24 22 23 mp1i ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑑 ∈ ω ) → { 𝑓𝐴𝑓𝑑 } ⊆ { 𝑓𝐴𝑓 ≼ suc 𝑑 } )
25 id ( 𝑑 ∈ ω → 𝑑 ∈ ω )
26 pwexg ( 𝐵 ∈ FinIII → 𝒫 𝐵 ∈ V )
27 26 adantl ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → 𝒫 𝐵 ∈ V )
28 27 2 ssexd ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → 𝐴 ∈ V )
29 rabexg ( 𝐴 ∈ V → { 𝑓𝐴𝑓𝑑 } ∈ V )
30 uniexg ( { 𝑓𝐴𝑓𝑑 } ∈ V → { 𝑓𝐴𝑓𝑑 } ∈ V )
31 28 29 30 3syl ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → { 𝑓𝐴𝑓𝑑 } ∈ V )
32 breq2 ( 𝑒 = 𝑑 → ( 𝑓𝑒𝑓𝑑 ) )
33 32 rabbidv ( 𝑒 = 𝑑 → { 𝑓𝐴𝑓𝑒 } = { 𝑓𝐴𝑓𝑑 } )
34 33 unieqd ( 𝑒 = 𝑑 { 𝑓𝐴𝑓𝑒 } = { 𝑓𝐴𝑓𝑑 } )
35 eqid ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } )
36 34 35 fvmptg ( ( 𝑑 ∈ ω ∧ { 𝑓𝐴𝑓𝑑 } ∈ V ) → ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ 𝑑 ) = { 𝑓𝐴𝑓𝑑 } )
37 25 31 36 syl2anr ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑑 ∈ ω ) → ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ 𝑑 ) = { 𝑓𝐴𝑓𝑑 } )
38 peano2 ( 𝑑 ∈ ω → suc 𝑑 ∈ ω )
39 rabexg ( 𝐴 ∈ V → { 𝑓𝐴𝑓 ≼ suc 𝑑 } ∈ V )
40 uniexg ( { 𝑓𝐴𝑓 ≼ suc 𝑑 } ∈ V → { 𝑓𝐴𝑓 ≼ suc 𝑑 } ∈ V )
41 28 39 40 3syl ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → { 𝑓𝐴𝑓 ≼ suc 𝑑 } ∈ V )
42 breq2 ( 𝑒 = suc 𝑑 → ( 𝑓𝑒𝑓 ≼ suc 𝑑 ) )
43 42 rabbidv ( 𝑒 = suc 𝑑 → { 𝑓𝐴𝑓𝑒 } = { 𝑓𝐴𝑓 ≼ suc 𝑑 } )
44 43 unieqd ( 𝑒 = suc 𝑑 { 𝑓𝐴𝑓𝑒 } = { 𝑓𝐴𝑓 ≼ suc 𝑑 } )
45 44 35 fvmptg ( ( suc 𝑑 ∈ ω ∧ { 𝑓𝐴𝑓 ≼ suc 𝑑 } ∈ V ) → ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ suc 𝑑 ) = { 𝑓𝐴𝑓 ≼ suc 𝑑 } )
46 38 41 45 syl2anr ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑑 ∈ ω ) → ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ suc 𝑑 ) = { 𝑓𝐴𝑓 ≼ suc 𝑑 } )
47 24 37 46 3sstr4d ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) ∧ 𝑑 ∈ ω ) → ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ 𝑑 ) ⊆ ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ suc 𝑑 ) )
48 47 ralrimiva ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ∀ 𝑑 ∈ ω ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ 𝑑 ) ⊆ ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ suc 𝑑 ) )
49 fin34i ( ( 𝐵 ∈ FinIII ∧ ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) : ω ⟶ 𝒫 𝐵 ∧ ∀ 𝑑 ∈ ω ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ 𝑑 ) ⊆ ( ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ‘ suc 𝑑 ) ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ∈ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) )
50 1 13 48 49 syl3anc ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ∈ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) )
51 fin1a2lem11 ( ( [] Or 𝐴𝐴 ⊆ Fin ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) )
52 51 adantrr ( ( [] Or 𝐴 ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) )
53 52 3ad2antl2 ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) )
54 53 adantr ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) )
55 simpll3 ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ¬ 𝐴𝐴 )
56 simplrr ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → 𝐴 ≠ ∅ )
57 sspwuni ( 𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ ∅ )
58 ss0b ( 𝐴 ⊆ ∅ ↔ 𝐴 = ∅ )
59 57 58 bitri ( 𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 = ∅ )
60 pw0 𝒫 ∅ = { ∅ }
61 60 sseq2i ( 𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ { ∅ } )
62 sssn ( 𝐴 ⊆ { ∅ } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { ∅ } ) )
63 61 62 bitri ( 𝐴 ⊆ 𝒫 ∅ ↔ ( 𝐴 = ∅ ∨ 𝐴 = { ∅ } ) )
64 df-ne ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
65 0ex ∅ ∈ V
66 65 unisn { ∅ } = ∅
67 65 snid ∅ ∈ { ∅ }
68 66 67 eqeltri { ∅ } ∈ { ∅ }
69 unieq ( 𝐴 = { ∅ } → 𝐴 = { ∅ } )
70 id ( 𝐴 = { ∅ } → 𝐴 = { ∅ } )
71 69 70 eleq12d ( 𝐴 = { ∅ } → ( 𝐴𝐴 { ∅ } ∈ { ∅ } ) )
72 68 71 mpbiri ( 𝐴 = { ∅ } → 𝐴𝐴 )
73 72 orim2i ( ( 𝐴 = ∅ ∨ 𝐴 = { ∅ } ) → ( 𝐴 = ∅ ∨ 𝐴𝐴 ) )
74 73 ord ( ( 𝐴 = ∅ ∨ 𝐴 = { ∅ } ) → ( ¬ 𝐴 = ∅ → 𝐴𝐴 ) )
75 64 74 syl5bi ( ( 𝐴 = ∅ ∨ 𝐴 = { ∅ } ) → ( 𝐴 ≠ ∅ → 𝐴𝐴 ) )
76 63 75 sylbi ( 𝐴 ⊆ 𝒫 ∅ → ( 𝐴 ≠ ∅ → 𝐴𝐴 ) )
77 59 76 sylbir ( 𝐴 = ∅ → ( 𝐴 ≠ ∅ → 𝐴𝐴 ) )
78 77 com12 ( 𝐴 ≠ ∅ → ( 𝐴 = ∅ → 𝐴𝐴 ) )
79 78 con3d ( 𝐴 ≠ ∅ → ( ¬ 𝐴𝐴 → ¬ 𝐴 = ∅ ) )
80 56 55 79 sylc ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ¬ 𝐴 = ∅ )
81 ioran ( ¬ ( 𝐴𝐴 𝐴 = ∅ ) ↔ ( ¬ 𝐴𝐴 ∧ ¬ 𝐴 = ∅ ) )
82 55 80 81 sylanbrc ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ¬ ( 𝐴𝐴 𝐴 = ∅ ) )
83 uniun ( 𝐴 ∪ { ∅ } ) = ( 𝐴 { ∅ } )
84 66 uneq2i ( 𝐴 { ∅ } ) = ( 𝐴 ∪ ∅ )
85 un0 ( 𝐴 ∪ ∅ ) = 𝐴
86 83 84 85 3eqtri ( 𝐴 ∪ { ∅ } ) = 𝐴
87 86 eleq1i ( ( 𝐴 ∪ { ∅ } ) ∈ ( 𝐴 ∪ { ∅ } ) ↔ 𝐴 ∈ ( 𝐴 ∪ { ∅ } ) )
88 elun ( 𝐴 ∈ ( 𝐴 ∪ { ∅ } ) ↔ ( 𝐴𝐴 𝐴 ∈ { ∅ } ) )
89 65 elsn2 ( 𝐴 ∈ { ∅ } ↔ 𝐴 = ∅ )
90 89 orbi2i ( ( 𝐴𝐴 𝐴 ∈ { ∅ } ) ↔ ( 𝐴𝐴 𝐴 = ∅ ) )
91 87 88 90 3bitri ( ( 𝐴 ∪ { ∅ } ) ∈ ( 𝐴 ∪ { ∅ } ) ↔ ( 𝐴𝐴 𝐴 = ∅ ) )
92 82 91 sylnibr ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ¬ ( 𝐴 ∪ { ∅ } ) ∈ ( 𝐴 ∪ { ∅ } ) )
93 unieq ( ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) )
94 id ( ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) → ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) )
95 93 94 eleq12d ( ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) → ( ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ∈ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ↔ ( 𝐴 ∪ { ∅ } ) ∈ ( 𝐴 ∪ { ∅ } ) ) )
96 95 notbid ( ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) → ( ¬ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ∈ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ↔ ¬ ( 𝐴 ∪ { ∅ } ) ∈ ( 𝐴 ∪ { ∅ } ) ) )
97 92 96 syl5ibrcom ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ( ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) = ( 𝐴 ∪ { ∅ } ) → ¬ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ∈ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ) )
98 54 97 mpd ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) ∧ 𝐵 ∈ FinIII ) → ¬ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) ∈ ran ( 𝑒 ∈ ω ↦ { 𝑓𝐴𝑓𝑒 } ) )
99 50 98 pm2.65da ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴 ) ∧ ( 𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅ ) ) → ¬ 𝐵 ∈ FinIII )