Metamath Proof Explorer

Theorem infmap2

Description: An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of Jech p. 43. Although this version of infmap avoids the axiom of choice, it requires the powerset of an infinite set to be well-orderable and so is usually not applicable. (Contributed by NM, 1-Oct-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion infmap2 ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝐵 = ∅ → ( 𝐴 ↑m 𝐵 ) = ( 𝐴 ↑m ∅ ) )
2 breq2 ⊢ ( 𝐵 = ∅ → ( 𝑥 ≈ 𝐵 ↔ 𝑥 ≈ ∅ ) )
3 2 anbi2d ⊢ ( 𝐵 = ∅ → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) ) )
4 3 abbidv ⊢ ( 𝐵 = ∅ → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) } )
5 1 4 breq12d ⊢ ( 𝐵 = ∅ → ( ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ↔ ( 𝐴 ↑m ∅ ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) } ) )
6 simpl2 ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → 𝐵 ≼ 𝐴 )
7 reldom ⊢ Rel ≼
8 7 brrelex1i ⊢ ( 𝐵 ≼ 𝐴 → 𝐵 ∈ V )
9 6 8 syl ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → 𝐵 ∈ V )
10 7 brrelex2i ⊢ ( 𝐵 ≼ 𝐴 → 𝐴 ∈ V )
11 6 10 syl ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → 𝐴 ∈ V )
12 xpcomeng ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) )
13 9 11 12 syl2anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) )
14 simpl3 ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ↑m 𝐵 ) ∈ dom card )
15 simpr ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → 𝐵 ≠ ∅ )
16 mapdom3 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )
17 11 9 15 16 syl3anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) )
18 numdom ⊢ ( ( ( 𝐴 ↑m 𝐵 ) ∈ dom card ∧ 𝐴 ≼ ( 𝐴 ↑m 𝐵 ) ) → 𝐴 ∈ dom card )
19 14 17 18 syl2anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → 𝐴 ∈ dom card )
20 simpl1 ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ω ≼ 𝐴 )
21 infxpabs ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ 𝐴 )
22 19 20 15 6 21 syl22anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≈ 𝐴 )
23 entr ⊢ ( ( ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) ∧ ( 𝐴 × 𝐵 ) ≈ 𝐴 ) → ( 𝐵 × 𝐴 ) ≈ 𝐴 )
24 13 22 23 syl2anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐵 × 𝐴 ) ≈ 𝐴 )
25 ssenen ⊢ ( ( 𝐵 × 𝐴 ) ≈ 𝐴 → { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
26 24 25 syl ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
27 relen ⊢ Rel ≈
28 27 brrelex1i ⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } → { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ∈ V )
29 26 28 syl ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ∈ V )
30 abid2 ⊢ { 𝑥 ∣ 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) } = ( 𝐴 ↑m 𝐵 )
31 elmapi ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) → 𝑥 : 𝐵 ⟶ 𝐴 )
32 fssxp ⊢ ( 𝑥 : 𝐵 ⟶ 𝐴 → 𝑥 ⊆ ( 𝐵 × 𝐴 ) )
33 ffun ⊢ ( 𝑥 : 𝐵 ⟶ 𝐴 → Fun 𝑥 )
34 vex ⊢ 𝑥 ∈ V
35 34 fundmen ⊢ ( Fun 𝑥 → dom 𝑥 ≈ 𝑥 )
36 ensym ⊢ ( dom 𝑥 ≈ 𝑥 → 𝑥 ≈ dom 𝑥 )
37 33 35 36 3syl ⊢ ( 𝑥 : 𝐵 ⟶ 𝐴 → 𝑥 ≈ dom 𝑥 )
38 fdm ⊢ ( 𝑥 : 𝐵 ⟶ 𝐴 → dom 𝑥 = 𝐵 )
39 37 38 breqtrd ⊢ ( 𝑥 : 𝐵 ⟶ 𝐴 → 𝑥 ≈ 𝐵 )
40 32 39 jca ⊢ ( 𝑥 : 𝐵 ⟶ 𝐴 → ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) )
41 31 40 syl ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) )
42 41 ss2abi ⊢ { 𝑥 ∣ 𝑥 ∈ ( 𝐴 ↑m 𝐵 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) }
43 30 42 eqsstrri ⊢ ( 𝐴 ↑m 𝐵 ) ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) }
44 ssdomg ⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ∈ V → ( ( 𝐴 ↑m 𝐵 ) ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } → ( 𝐴 ↑m 𝐵 ) ≼ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ) )
45 29 43 44 mpisyl ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ↑m 𝐵 ) ≼ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } )
46 domentr ⊢ ( ( ( 𝐴 ↑m 𝐵 ) ≼ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ∧ { 𝑥 ∣ ( 𝑥 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑥 ≈ 𝐵 ) } ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ) → ( 𝐴 ↑m 𝐵 ) ≼ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
47 45 26 46 syl2anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ↑m 𝐵 ) ≼ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
48 ovex ⊢ ( 𝐴 ↑m 𝐵 ) ∈ V
49 48 mptex ⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ∈ V
50 49 rnex ⊢ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ∈ V
51 ensym ⊢ ( 𝑥 ≈ 𝐵 → 𝐵 ≈ 𝑥 )
52 51 ad2antll ⊢ ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) → 𝐵 ≈ 𝑥 )
53 bren ⊢ ( 𝐵 ≈ 𝑥 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝑥 )
54 52 53 sylib ⊢ ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) → ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝑥 )
55 f1of ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝑥 → 𝑓 : 𝐵 ⟶ 𝑥 )
56 55 adantl ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → 𝑓 : 𝐵 ⟶ 𝑥 )
57 simplrl ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → 𝑥 ⊆ 𝐴 )
58 56 57 fssd ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → 𝑓 : 𝐵 ⟶ 𝐴 )
59 11 9 elmapd ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝑓 : 𝐵 ⟶ 𝐴 ) )
60 59 ad2antrr ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝑓 : 𝐵 ⟶ 𝐴 ) )
61 58 60 mpbird ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) )
62 f1ofo ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝑥 → 𝑓 : 𝐵 –onto→ 𝑥 )
63 forn ⊢ ( 𝑓 : 𝐵 –onto→ 𝑥 → ran 𝑓 = 𝑥 )
64 62 63 syl ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝑥 → ran 𝑓 = 𝑥 )
65 64 adantl ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → ran 𝑓 = 𝑥 )
66 65 eqcomd ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → 𝑥 = ran 𝑓 )
67 61 66 jca ⊢ ( ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) ∧ 𝑓 : 𝐵 –1-1-onto→ 𝑥 ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝑥 = ran 𝑓 ) )
68 67 ex ⊢ ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑓 : 𝐵 –1-1-onto→ 𝑥 → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝑥 = ran 𝑓 ) ) )
69 68 eximdv ⊢ ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) → ( ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝑥 → ∃ 𝑓 ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝑥 = ran 𝑓 ) ) )
70 54 69 mpd ⊢ ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) → ∃ 𝑓 ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝑥 = ran 𝑓 ) )
71 df-rex ⊢ ( ∃ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) 𝑥 = ran 𝑓 ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ∧ 𝑥 = ran 𝑓 ) )
72 70 71 sylibr ⊢ ( ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) ) → ∃ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) 𝑥 = ran 𝑓 )
73 72 ex ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) → ∃ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) 𝑥 = ran 𝑓 ) )
74 73 ss2abdv ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ⊆ { 𝑥 ∣ ∃ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) 𝑥 = ran 𝑓 } )
75 eqid ⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) = ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 )
76 75 rnmpt ⊢ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) = { 𝑥 ∣ ∃ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) 𝑥 = ran 𝑓 }
77 74 76 sseqtrrdi ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ⊆ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) )
78 ssdomg ⊢ ( ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ∈ V → ( { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ⊆ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ≼ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ) )
79 50 77 78 mpsyl ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ≼ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) )
80 vex ⊢ 𝑓 ∈ V
81 80 rnex ⊢ ran 𝑓 ∈ V
82 81 rgenw ⊢ ∀ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ran 𝑓 ∈ V
83 75 fnmpt ⊢ ( ∀ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ran 𝑓 ∈ V → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) Fn ( 𝐴 ↑m 𝐵 ) )
84 82 83 mp1i ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) Fn ( 𝐴 ↑m 𝐵 ) )
85 dffn4 ⊢ ( ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) Fn ( 𝐴 ↑m 𝐵 ) ↔ ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) : ( 𝐴 ↑m 𝐵 ) –onto→ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) )
86 84 85 sylib ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) : ( 𝐴 ↑m 𝐵 ) –onto→ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) )
87 fodomnum ⊢ ( ( 𝐴 ↑m 𝐵 ) ∈ dom card → ( ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) : ( 𝐴 ↑m 𝐵 ) –onto→ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) → ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ≼ ( 𝐴 ↑m 𝐵 ) ) )
88 14 86 87 sylc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ≼ ( 𝐴 ↑m 𝐵 ) )
89 domtr ⊢ ( ( { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ≼ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ∧ ran ( 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↦ ran 𝑓 ) ≼ ( 𝐴 ↑m 𝐵 ) ) → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ≼ ( 𝐴 ↑m 𝐵 ) )
90 79 88 89 syl2anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ≼ ( 𝐴 ↑m 𝐵 ) )
91 sbth ⊢ ( ( ( 𝐴 ↑m 𝐵 ) ≼ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ∧ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } ≼ ( 𝐴 ↑m 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
92 47 90 91 syl2anc ⊢ ( ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )
93 7 brrelex2i ⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
94 93 3ad2ant1 ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) → 𝐴 ∈ V )
95 map0e ⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m ∅ ) = 1o )
96 94 95 syl ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) → ( 𝐴 ↑m ∅ ) = 1o )
97 1oex ⊢ 1o ∈ V
98 97 enref ⊢ 1o ≈ 1o
99 df-sn ⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
100 df1o2 ⊢ 1o = { ∅ }
101 en0 ⊢ ( 𝑥 ≈ ∅ ↔ 𝑥 = ∅ )
102 101 anbi2i ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅ ) )
103 0ss ⊢ ∅ ⊆ 𝐴
104 sseq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
105 103 104 mpbiri ⊢ ( 𝑥 = ∅ → 𝑥 ⊆ 𝐴 )
106 105 pm4.71ri ⊢ ( 𝑥 = ∅ ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅ ) )
107 102 106 bitr4i ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) ↔ 𝑥 = ∅ )
108 107 abbii ⊢ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) } = { 𝑥 ∣ 𝑥 = ∅ }
109 99 100 108 3eqtr4ri ⊢ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) } = 1o
110 98 109 breqtrri ⊢ 1o ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) }
111 96 110 eqbrtrdi ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) → ( 𝐴 ↑m ∅ ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) } )
112 5 92 111 pm2.61ne ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ ( 𝐴 ↑m 𝐵 ) ∈ dom card ) → ( 𝐴 ↑m 𝐵 ) ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵 ) } )