This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin1a2lem11

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem11 ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ran ( 𝑏 ∈ ω ↦ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) = ( 𝐴 ∪ { ∅ } ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑏 ∈ ω ↦ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) = ( 𝑏 ∈ ω ↦ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
2 1 rnmpt ⊢ ran ( 𝑏 ∈ ω ↦ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) = { 𝑑 ∣ ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } }
3 unieq ⊢ ( { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∪ ∅ )
4 uni0 ⊢ ∪ ∅ = ∅
5 3 4 eqtrdi ⊢ ( { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ )
6 5 adantl ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ )
7 0ex ⊢ ∅ ∈ V
8 7 elsn2 ⊢ ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } ↔ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ )
9 6 8 sylibr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } )
10 9 olcd ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∅ ) → ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ 𝐴 ∨ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } ) )
11 ssrab2 ⊢ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ⊆ 𝐴
12 simpr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ )
13 fin1a2lem9 ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ∧ 𝑏 ∈ ω ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ Fin )
14 13 ad4ant123 ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ Fin )
15 simplll ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → [⊊] Or 𝐴 )
16 soss ⊢ ( { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ⊆ 𝐴 → ( [⊊] Or 𝐴 → [⊊] Or { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
17 11 15 16 mpsyl ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → [⊊] Or { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
18 fin1a2lem10 ⊢ ( ( { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ Fin ∧ [⊊] Or { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
19 12 14 17 18 syl3anc ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
20 11 19 sselid ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ 𝐴 )
21 20 orcd ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) ∧ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ≠ ∅ ) → ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ 𝐴 ∨ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } ) )
22 10 21 pm2.61dane ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) → ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ 𝐴 ∨ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } ) )
23 eleq1 ⊢ ( 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } → ( 𝑑 ∈ 𝐴 ↔ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ 𝐴 ) )
24 eleq1 ⊢ ( 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } → ( 𝑑 ∈ { ∅ } ↔ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } ) )
25 23 24 orbi12d ⊢ ( 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } → ( ( 𝑑 ∈ 𝐴 ∨ 𝑑 ∈ { ∅ } ) ↔ ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ 𝐴 ∨ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ∈ { ∅ } ) ) )
26 22 25 syl5ibrcom ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑏 ∈ ω ) → ( 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } → ( 𝑑 ∈ 𝐴 ∨ 𝑑 ∈ { ∅ } ) ) )
27 26 rexlimdva ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } → ( 𝑑 ∈ 𝐴 ∨ 𝑑 ∈ { ∅ } ) ) )
28 simpr ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ Fin )
29 28 sselda ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → 𝑑 ∈ Fin )
30 ficardom ⊢ ( 𝑑 ∈ Fin → ( card ‘ 𝑑 ) ∈ ω )
31 29 30 syl ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ( card ‘ 𝑑 ) ∈ ω )
32 breq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ≼ ( card ‘ 𝑑 ) ↔ 𝑑 ≼ ( card ‘ 𝑑 ) ) )
33 simpr ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → 𝑑 ∈ 𝐴 )
34 ficardid ⊢ ( 𝑑 ∈ Fin → ( card ‘ 𝑑 ) ≈ 𝑑 )
35 29 34 syl ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ( card ‘ 𝑑 ) ≈ 𝑑 )
36 ensym ⊢ ( ( card ‘ 𝑑 ) ≈ 𝑑 → 𝑑 ≈ ( card ‘ 𝑑 ) )
37 endom ⊢ ( 𝑑 ≈ ( card ‘ 𝑑 ) → 𝑑 ≼ ( card ‘ 𝑑 ) )
38 35 36 37 3syl ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → 𝑑 ≼ ( card ‘ 𝑑 ) )
39 32 33 38 elrabd ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → 𝑑 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } )
40 elssuni ⊢ ( 𝑑 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } → 𝑑 ⊆ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } )
41 39 40 syl ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → 𝑑 ⊆ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } )
42 breq1 ⊢ ( 𝑐 = 𝑏 → ( 𝑐 ≼ ( card ‘ 𝑑 ) ↔ 𝑏 ≼ ( card ‘ 𝑑 ) ) )
43 42 elrab ⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } ↔ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) )
44 simprr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑏 ≼ ( card ‘ 𝑑 ) )
45 35 adantr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → ( card ‘ 𝑑 ) ≈ 𝑑 )
46 domentr ⊢ ( ( 𝑏 ≼ ( card ‘ 𝑑 ) ∧ ( card ‘ 𝑑 ) ≈ 𝑑 ) → 𝑏 ≼ 𝑑 )
47 44 45 46 syl2anc ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑏 ≼ 𝑑 )
48 simpllr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝐴 ⊆ Fin )
49 simprl ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑏 ∈ 𝐴 )
50 48 49 sseldd ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑏 ∈ Fin )
51 29 adantr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑑 ∈ Fin )
52 simplll ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → [⊊] Or 𝐴 )
53 simplr ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑑 ∈ 𝐴 )
54 sorpssi ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( 𝑏 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑏 ) )
55 52 49 53 54 syl12anc ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → ( 𝑏 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑏 ) )
56 fincssdom ⊢ ( ( 𝑏 ∈ Fin ∧ 𝑑 ∈ Fin ∧ ( 𝑏 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑏 ) ) → ( 𝑏 ≼ 𝑑 ↔ 𝑏 ⊆ 𝑑 ) )
57 50 51 55 56 syl3anc ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → ( 𝑏 ≼ 𝑑 ↔ 𝑏 ⊆ 𝑑 ) )
58 47 57 mpbid ⊢ ( ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) ) → 𝑏 ⊆ 𝑑 )
59 58 ex ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ( card ‘ 𝑑 ) ) → 𝑏 ⊆ 𝑑 ) )
60 43 59 biimtrid ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ( 𝑏 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } → 𝑏 ⊆ 𝑑 ) )
61 60 ralrimiv ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ∀ 𝑏 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } 𝑏 ⊆ 𝑑 )
62 unissb ⊢ ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } ⊆ 𝑑 ↔ ∀ 𝑏 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } 𝑏 ⊆ 𝑑 )
63 61 62 sylibr ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } ⊆ 𝑑 )
64 41 63 eqssd ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } )
65 breq2 ⊢ ( 𝑏 = ( card ‘ 𝑑 ) → ( 𝑐 ≼ 𝑏 ↔ 𝑐 ≼ ( card ‘ 𝑑 ) ) )
66 65 rabbidv ⊢ ( 𝑏 = ( card ‘ 𝑑 ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } )
67 66 unieqd ⊢ ( 𝑏 = ( card ‘ 𝑑 ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } )
68 67 rspceeqv ⊢ ( ( ( card ‘ 𝑑 ) ∈ ω ∧ 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ( card ‘ 𝑑 ) } ) → ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
69 31 64 68 syl2anc ⊢ ( ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) ∧ 𝑑 ∈ 𝐴 ) → ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
70 69 ex ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑑 ∈ 𝐴 → ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
71 velsn ⊢ ( 𝑑 ∈ { ∅ } ↔ 𝑑 = ∅ )
72 peano1 ⊢ ∅ ∈ ω
73 dom0 ⊢ ( 𝑏 ≼ ∅ ↔ 𝑏 = ∅ )
74 73 biimpi ⊢ ( 𝑏 ≼ ∅ → 𝑏 = ∅ )
75 74 adantl ⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ∅ ) → 𝑏 = ∅ )
76 75 a1i ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ∅ ) → 𝑏 = ∅ ) )
77 breq1 ⊢ ( 𝑐 = 𝑏 → ( 𝑐 ≼ ∅ ↔ 𝑏 ≼ ∅ ) )
78 77 elrab ⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } ↔ ( 𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ∅ ) )
79 velsn ⊢ ( 𝑏 ∈ { ∅ } ↔ 𝑏 = ∅ )
80 76 78 79 3imtr4g ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑏 ∈ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } → 𝑏 ∈ { ∅ } ) )
81 80 ssrdv ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } ⊆ { ∅ } )
82 uni0b ⊢ ( ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } = ∅ ↔ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } ⊆ { ∅ } )
83 81 82 sylibr ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } = ∅ )
84 83 eqcomd ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ∅ = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } )
85 breq2 ⊢ ( 𝑏 = ∅ → ( 𝑐 ≼ 𝑏 ↔ 𝑐 ≼ ∅ ) )
86 85 rabbidv ⊢ ( 𝑏 = ∅ → { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } )
87 86 unieqd ⊢ ( 𝑏 = ∅ → ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } )
88 87 rspceeqv ⊢ ( ( ∅ ∈ ω ∧ ∅ = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅ } ) → ∃ 𝑏 ∈ ω ∅ = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
89 72 84 88 sylancr ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ∃ 𝑏 ∈ ω ∅ = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } )
90 eqeq1 ⊢ ( 𝑑 = ∅ → ( 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ↔ ∅ = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
91 90 rexbidv ⊢ ( 𝑑 = ∅ → ( ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ↔ ∃ 𝑏 ∈ ω ∅ = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
92 89 91 syl5ibrcom ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑑 = ∅ → ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
93 71 92 biimtrid ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑑 ∈ { ∅ } → ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
94 70 93 jaod ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( ( 𝑑 ∈ 𝐴 ∨ 𝑑 ∈ { ∅ } ) → ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) )
95 27 94 impbid ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ↔ ( 𝑑 ∈ 𝐴 ∨ 𝑑 ∈ { ∅ } ) ) )
96 elun ⊢ ( 𝑑 ∈ ( 𝐴 ∪ { ∅ } ) ↔ ( 𝑑 ∈ 𝐴 ∨ 𝑑 ∈ { ∅ } ) )
97 95 96 bitr4di ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ( ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ↔ 𝑑 ∈ ( 𝐴 ∪ { ∅ } ) ) )
98 97 eqabcdv ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → { 𝑑 ∣ ∃ 𝑏 ∈ ω 𝑑 = ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } } = ( 𝐴 ∪ { ∅ } ) )
99 2 98 eqtrid ⊢ ( ( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin ) → ran ( 𝑏 ∈ ω ↦ ∪ { 𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏 } ) = ( 𝐴 ∪ { ∅ } ) )