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

Metamath Proof Explorer

Theorem cfslb2n

Description: Any small collection of small subsets of A cannot have union A , where "small" means smaller than the cofinality. This is a stronger version of cfslb . This is a common application of cofinality: under AC, ( aleph1 ) is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis cfslb.1 ⊢ 𝐴 ∈ V
Assertion cfslb2n ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ∪ 𝐵 ≠ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cfslb.1 ⊢ 𝐴 ∈ V
2 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
3 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
4 sstr ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ On ) → 𝑥 ⊆ On )
5 4 expcom ⊢ ( 𝐴 ⊆ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ On ) )
6 2 3 5 3syl ⊢ ( Lim 𝐴 → ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ On ) )
7 onsucuni ⊢ ( 𝑥 ⊆ On → 𝑥 ⊆ suc ∪ 𝑥 )
8 6 7 syl6 ⊢ ( Lim 𝐴 → ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ suc ∪ 𝑥 ) )
9 8 adantrd ⊢ ( Lim 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → 𝑥 ⊆ suc ∪ 𝑥 ) )
10 9 ralimdv ⊢ ( Lim 𝐴 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪ 𝑥 ) )
11 uniiun ⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
12 ss2iun ⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪ 𝑥 → ∪ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 )
13 11 12 eqsstrid ⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ suc ∪ 𝑥 → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 )
14 10 13 syl6 ⊢ ( Lim 𝐴 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ) )
15 14 imp ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 )
16 1 cfslbn ⊢ ( ( Lim 𝐴 ∧ 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∪ 𝑥 ∈ 𝐴 )
17 16 3expib ⊢ ( Lim 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∪ 𝑥 ∈ 𝐴 ) )
18 ordsucss ⊢ ( Ord 𝐴 → ( ∪ 𝑥 ∈ 𝐴 → suc ∪ 𝑥 ⊆ 𝐴 ) )
19 2 17 18 sylsyld ⊢ ( Lim 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → suc ∪ 𝑥 ⊆ 𝐴 ) )
20 19 ralimdv ⊢ ( Lim 𝐴 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ) )
21 iunss ⊢ ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ↔ ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 )
22 20 21 imbitrrdi ⊢ ( Lim 𝐴 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ) )
23 22 imp ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 )
24 sseq1 ⊢ ( ∪ 𝐵 = 𝐴 → ( ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ↔ 𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ) )
25 eqss ⊢ ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ↔ ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ) )
26 25 simplbi2com ⊢ ( 𝐴 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ) )
27 24 26 biimtrdi ⊢ ( ∪ 𝐵 = 𝐴 → ( ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ) ) )
28 27 com3l ⊢ ( ∪ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 → ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ⊆ 𝐴 → ( ∪ 𝐵 = 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ) ) )
29 15 23 28 sylc ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( ∪ 𝐵 = 𝐴 → ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ) )
30 limsuc ⊢ ( Lim 𝐴 → ( ∪ 𝑥 ∈ 𝐴 ↔ suc ∪ 𝑥 ∈ 𝐴 ) )
31 17 30 sylibd ⊢ ( Lim 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → suc ∪ 𝑥 ∈ 𝐴 ) )
32 31 ralimdv ⊢ ( Lim 𝐴 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 ) )
33 32 imp ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 )
34 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 ) → ∃ 𝑥 ∈ 𝐵 ( suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥 ) )
35 eleq1 ⊢ ( 𝑦 = suc ∪ 𝑥 → ( 𝑦 ∈ 𝐴 ↔ suc ∪ 𝑥 ∈ 𝐴 ) )
36 35 biimparc ⊢ ( ( suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥 ) → 𝑦 ∈ 𝐴 )
37 36 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( suc ∪ 𝑥 ∈ 𝐴 ∧ 𝑦 = suc ∪ 𝑥 ) → 𝑦 ∈ 𝐴 )
38 34 37 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 ) → 𝑦 ∈ 𝐴 )
39 38 ex ⊢ ( ∀ 𝑥 ∈ 𝐵 suc ∪ 𝑥 ∈ 𝐴 → ( ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 → 𝑦 ∈ 𝐴 ) )
40 33 39 syl ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 → 𝑦 ∈ 𝐴 ) )
41 40 abssdv ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ⊆ 𝐴 )
42 vuniex ⊢ ∪ 𝑥 ∈ V
43 42 sucex ⊢ suc ∪ 𝑥 ∈ V
44 43 dfiun2 ⊢ ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 }
45 44 eqeq1i ⊢ ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 ↔ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } = 𝐴 )
46 1 cfslb ⊢ ( ( Lim 𝐴 ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ⊆ 𝐴 ∧ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } = 𝐴 ) → ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } )
47 46 3expia ⊢ ( ( Lim 𝐴 ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ⊆ 𝐴 ) → ( ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } = 𝐴 → ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ) )
48 45 47 biimtrid ⊢ ( ( Lim 𝐴 ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ⊆ 𝐴 ) → ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 → ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ) )
49 41 48 syldan ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( ∪ 𝑥 ∈ 𝐵 suc ∪ 𝑥 = 𝐴 → ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ) )
50 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) = ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 )
51 50 rnmpt ⊢ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 }
52 43 50 fnmpti ⊢ ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) Fn 𝐵
53 dffn4 ⊢ ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) Fn 𝐵 ↔ ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) )
54 52 53 mpbi ⊢ ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 )
55 relsdom ⊢ Rel ≺
56 55 brrelex1i ⊢ ( 𝐵 ≺ ( cf ‘ 𝐴 ) → 𝐵 ∈ V )
57 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ≺ ( cf ‘ 𝐴 ) ↔ 𝐵 ≺ ( cf ‘ 𝐴 ) ) )
58 foeq2 ⊢ ( 𝑦 = 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ) )
59 breq2 ⊢ ( 𝑦 = 𝐵 → ( ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝑦 ↔ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝐵 ) )
60 58 59 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝐵 ) ) )
61 57 60 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ≺ ( cf ‘ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝑦 ) ) ↔ ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝐵 ) ) ) )
62 cfon ⊢ ( cf ‘ 𝐴 ) ∈ On
63 sdomdom ⊢ ( 𝑦 ≺ ( cf ‘ 𝐴 ) → 𝑦 ≼ ( cf ‘ 𝐴 ) )
64 ondomen ⊢ ( ( ( cf ‘ 𝐴 ) ∈ On ∧ 𝑦 ≼ ( cf ‘ 𝐴 ) ) → 𝑦 ∈ dom card )
65 62 63 64 sylancr ⊢ ( 𝑦 ≺ ( cf ‘ 𝐴 ) → 𝑦 ∈ dom card )
66 fodomnum ⊢ ( 𝑦 ∈ dom card → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝑦 ) )
67 65 66 syl ⊢ ( 𝑦 ≺ ( cf ‘ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝑦 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝑦 ) )
68 61 67 vtoclg ⊢ ( 𝐵 ∈ V → ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝐵 ) ) )
69 56 68 mpcom ⊢ ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) : 𝐵 –onto→ ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝐵 ) )
70 54 69 mpi ⊢ ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ran ( 𝑥 ∈ 𝐵 ↦ suc ∪ 𝑥 ) ≼ 𝐵 )
71 51 70 eqbrtrrid ⊢ ( 𝐵 ≺ ( cf ‘ 𝐴 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ≼ 𝐵 )
72 domtr ⊢ ( ( ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ≼ 𝐵 ) → ( cf ‘ 𝐴 ) ≼ 𝐵 )
73 71 72 sylan2 ⊢ ( ( ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ∧ 𝐵 ≺ ( cf ‘ 𝐴 ) ) → ( cf ‘ 𝐴 ) ≼ 𝐵 )
74 domnsym ⊢ ( ( cf ‘ 𝐴 ) ≼ 𝐵 → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) )
75 73 74 syl ⊢ ( ( ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } ∧ 𝐵 ≺ ( cf ‘ 𝐴 ) ) → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) )
76 75 pm2.01da ⊢ ( ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) )
77 76 a1i ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( ( cf ‘ 𝐴 ) ≼ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = suc ∪ 𝑥 } → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) ) )
78 29 49 77 3syld ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( ∪ 𝐵 = 𝐴 → ¬ 𝐵 ≺ ( cf ‘ 𝐴 ) ) )
79 78 necon2ad ⊢ ( ( Lim 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ ( cf ‘ 𝐴 ) ) ) → ( 𝐵 ≺ ( cf ‘ 𝐴 ) → ∪ 𝐵 ≠ 𝐴 ) )