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 )