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 biimtrid ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = { ∅ } ) → ( 𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴 ) )
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 )