Metamath Proof Explorer

Theorem dfac12lem3

Description: Lemma for dfac12 . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Hypotheses dfac12.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
dfac12.3 ⊢ ( 𝜑 → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On )
dfac12.4 ⊢ 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) )
Assertion dfac12lem3 ( 𝜑 → ( 𝑅1 ‘ 𝐴 ) ∈ dom card )

Proof

Step Hyp Ref Expression
1 dfac12.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 dfac12.3 ⊢ ( 𝜑 → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On )
3 dfac12.4 ⊢ 𝐺 = recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝐹 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) )
4 fvex ⊢ ( 𝐺 ‘ 𝐴 ) ∈ V
5 4 rnex ⊢ ran ( 𝐺 ‘ 𝐴 ) ∈ V
6 ssid ⊢ 𝐴 ⊆ 𝐴
7 sseq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ⊆ 𝐴 ↔ 𝑛 ⊆ 𝐴 ) )
8 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑛 ) )
9 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑛 ) → ( ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) )
10 8 9 syl ⊢ ( 𝑚 = 𝑛 → ( ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) )
11 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑅1 ‘ 𝑚 ) = ( 𝑅1 ‘ 𝑛 ) )
12 f1eq2 ⊢ ( ( 𝑅1 ‘ 𝑚 ) = ( 𝑅1 ‘ 𝑛 ) → ( ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
13 11 12 syl ⊢ ( 𝑚 = 𝑛 → ( ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
14 10 13 bitrd ⊢ ( 𝑚 = 𝑛 → ( ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
15 7 14 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ↔ ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ) )
16 15 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝜑 → ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) ↔ ( 𝜑 → ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ) ) )
17 sseq1 ⊢ ( 𝑚 = 𝐴 → ( 𝑚 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
18 fveq2 ⊢ ( 𝑚 = 𝐴 → ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝐴 ) )
19 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑚 ) = ( 𝐺 ‘ 𝐴 ) → ( ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) )
20 18 19 syl ⊢ ( 𝑚 = 𝐴 → ( ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) )
21 fveq2 ⊢ ( 𝑚 = 𝐴 → ( 𝑅1 ‘ 𝑚 ) = ( 𝑅1 ‘ 𝐴 ) )
22 f1eq2 ⊢ ( ( 𝑅1 ‘ 𝑚 ) = ( 𝑅1 ‘ 𝐴 ) → ( ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) )
23 21 22 syl ⊢ ( 𝑚 = 𝐴 → ( ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) )
24 20 23 bitrd ⊢ ( 𝑚 = 𝐴 → ( ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ↔ ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) )
25 17 24 imbi12d ⊢ ( 𝑚 = 𝐴 → ( ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ↔ ( 𝐴 ⊆ 𝐴 → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) ) )
26 25 imbi2d ⊢ ( 𝑚 = 𝐴 → ( ( 𝜑 → ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) ↔ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) ) ) )
27 r19.21v ⊢ ( ∀ 𝑛 ∈ 𝑚 ( 𝜑 → ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ) ↔ ( 𝜑 → ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ) )
28 eloni ⊢ ( 𝑚 ∈ On → Ord 𝑚 )
29 28 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) → Ord 𝑚 )
30 ordelss ⊢ ( ( Ord 𝑚 ∧ 𝑛 ∈ 𝑚 ) → 𝑛 ⊆ 𝑚 )
31 29 30 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ 𝑛 ∈ 𝑚 ) → 𝑛 ⊆ 𝑚 )
32 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ 𝑛 ∈ 𝑚 ) → 𝑚 ⊆ 𝐴 )
33 31 32 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ 𝑛 ∈ 𝑚 ) → 𝑛 ⊆ 𝐴 )
34 pm5.5 ⊢ ( 𝑛 ⊆ 𝐴 → ( ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ 𝑛 ∈ 𝑚 ) → ( ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ↔ ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
36 35 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) → ( ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ↔ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
37 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → 𝐴 ∈ On )
38 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → 𝐹 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝐴 ) ) –1-1→ On )
39 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → 𝑚 ∈ On )
40 eqid ⊢ ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝑚 ) ) ∘ ( 𝐺 ‘ ∪ 𝑚 ) ) = ( ◡ OrdIso ( E , ran ( 𝐺 ‘ ∪ 𝑚 ) ) ∘ ( 𝐺 ‘ ∪ 𝑚 ) )
41 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → 𝑚 ⊆ 𝐴 )
42 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On )
43 fveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑧 ) )
44 f1eq1 ⊢ ( ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑧 ) → ( ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
45 43 44 syl ⊢ ( 𝑛 = 𝑧 → ( ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) )
46 fveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝑅1 ‘ 𝑛 ) = ( 𝑅1 ‘ 𝑧 ) )
47 f1eq2 ⊢ ( ( 𝑅1 ‘ 𝑛 ) = ( 𝑅1 ‘ 𝑧 ) → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) )
48 46 47 syl ⊢ ( 𝑛 = 𝑧 → ( ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) )
49 45 48 bitrd ⊢ ( 𝑛 = 𝑧 → ( ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ↔ ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On ) )
50 49 cbvralvw ⊢ ( ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ↔ ∀ 𝑧 ∈ 𝑚 ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On )
51 42 50 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ∀ 𝑧 ∈ 𝑚 ( 𝐺 ‘ 𝑧 ) : ( 𝑅1 ‘ 𝑧 ) –1-1→ On )
52 37 38 3 39 40 41 51 dfac12lem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) ∧ ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On )
53 52 ex ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) → ( ∀ 𝑛 ∈ 𝑚 ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) )
54 36 53 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ On ∧ 𝑚 ⊆ 𝐴 ) ) → ( ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) )
55 54 expr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ On ) → ( 𝑚 ⊆ 𝐴 → ( ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) )
56 55 com23 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ On ) → ( ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) )
57 56 expcom ⊢ ( 𝑚 ∈ On → ( 𝜑 → ( ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) → ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) ) )
58 57 a2d ⊢ ( 𝑚 ∈ On → ( ( 𝜑 → ∀ 𝑛 ∈ 𝑚 ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ) → ( 𝜑 → ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) ) )
59 27 58 biimtrid ⊢ ( 𝑚 ∈ On → ( ∀ 𝑛 ∈ 𝑚 ( 𝜑 → ( 𝑛 ⊆ 𝐴 → ( 𝐺 ‘ 𝑛 ) : ( 𝑅1 ‘ 𝑛 ) –1-1→ On ) ) → ( 𝜑 → ( 𝑚 ⊆ 𝐴 → ( 𝐺 ‘ 𝑚 ) : ( 𝑅1 ‘ 𝑚 ) –1-1→ On ) ) ) )
60 16 26 59 tfis3 ⊢ ( 𝐴 ∈ On → ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) ) )
61 1 60 mpcom ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On ) )
62 6 61 mpi ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On )
63 f1f ⊢ ( ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) ⟶ On )
64 frn ⊢ ( ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) ⟶ On → ran ( 𝐺 ‘ 𝐴 ) ⊆ On )
65 62 63 64 3syl ⊢ ( 𝜑 → ran ( 𝐺 ‘ 𝐴 ) ⊆ On )
66 onssnum ⊢ ( ( ran ( 𝐺 ‘ 𝐴 ) ∈ V ∧ ran ( 𝐺 ‘ 𝐴 ) ⊆ On ) → ran ( 𝐺 ‘ 𝐴 ) ∈ dom card )
67 5 65 66 sylancr ⊢ ( 𝜑 → ran ( 𝐺 ‘ 𝐴 ) ∈ dom card )
68 f1f1orn ⊢ ( ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1→ On → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1-onto→ ran ( 𝐺 ‘ 𝐴 ) )
69 62 68 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1-onto→ ran ( 𝐺 ‘ 𝐴 ) )
70 fvex ⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
71 70 f1oen ⊢ ( ( 𝐺 ‘ 𝐴 ) : ( 𝑅1 ‘ 𝐴 ) –1-1-onto→ ran ( 𝐺 ‘ 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ≈ ran ( 𝐺 ‘ 𝐴 ) )
72 ennum ⊢ ( ( 𝑅1 ‘ 𝐴 ) ≈ ran ( 𝐺 ‘ 𝐴 ) → ( ( 𝑅1 ‘ 𝐴 ) ∈ dom card ↔ ran ( 𝐺 ‘ 𝐴 ) ∈ dom card ) )
73 69 71 72 3syl ⊢ ( 𝜑 → ( ( 𝑅1 ‘ 𝐴 ) ∈ dom card ↔ ran ( 𝐺 ‘ 𝐴 ) ∈ dom card ) )
74 67 73 mpbird ⊢ ( 𝜑 → ( 𝑅1 ‘ 𝐴 ) ∈ dom card )