fuciso

Description: A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	fuciso.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fuciso.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fuciso.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	fuciso.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	fuciso.i	⊢ 𝐼 = ( Iso ‘ 𝑄 )
	fuciso.j	⊢ 𝐽 = ( Iso ‘ 𝐷 )
Assertion	fuciso	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ↔ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuciso.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		fuciso.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4		fuciso.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		fuciso.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
6		fuciso.i	⊢ 𝐼 = ( Iso ‘ 𝑄 )
7		fuciso.j	⊢ 𝐽 = ( Iso ‘ 𝐷 )
8	1	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
9	1 3	fuchom	⊢ 𝑁 = ( Hom ‘ 𝑄 )
10		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
11	4 10	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
12	11	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13	11	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14	1 12 13	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
15	8 9 6 14 4 5	isohom	⊢ ( 𝜑 → ( 𝐹 𝐼 𝐺 ) ⊆ ( 𝐹 𝑁 𝐺 ) )
16	15	sselda	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
17		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18		eqid	⊢ ( Inv ‘ 𝐷 ) = ( Inv ‘ 𝐷 )
19	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ Cat )
20		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
21		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
22	20 4 21	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
23	2 17 22	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
25	24	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
26		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
27	20 5 26	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
28	2 17 27	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
30	29	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
31		eqid	⊢ ( Inv ‘ 𝑄 ) = ( Inv ‘ 𝑄 )
32	8 31 14 4 5 6	isoval	⊢ ( 𝜑 → ( 𝐹 𝐼 𝐺 ) = dom ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) )
33	32	eleq2d	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ↔ 𝐴 ∈ dom ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ) )
34	8 31 14 4 5	invfun	⊢ ( 𝜑 → Fun ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) )
35		funfvbrb	⊢ ( Fun ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ↔ 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ) )
36	34 35	syl	⊢ ( 𝜑 → ( 𝐴 ∈ dom ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ↔ 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ) )
37	33 36	bitrd	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ↔ 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ) )
38	37	biimpa	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) )
39	1 2 3 4 5 31 18	fucinv	⊢ ( 𝜑 → ( 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ↔ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ‘ 𝑥 ) ) ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ( 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ↔ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ‘ 𝑥 ) ) ) )
41	38 40	mpbid	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ‘ 𝑥 ) ) )
42	41	simp3d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ‘ 𝑥 ) )
43	42	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ‘ 𝐴 ) ‘ 𝑥 ) )
44	17 18 19 25 30 7 43	inviso1	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
45	44	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
46	16 45	jca	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ) → ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
47	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → 𝑄 ∈ Cat )
48	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
49	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
50		simprl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
51	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ Cat )
52	23	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
53	52	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
54	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
55	54	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
56		simprr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
57		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) )
58		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
59		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) )
60	58 59	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
61	57 60	eleq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ↔ ( 𝐴 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
62	61	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
63	56 62	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
64	17 7 18 51 53 55 63	invisoinvr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ ( 𝐴 ‘ 𝑦 ) ) )
65	1 2 3 48 49 31 18 50 64	invfuc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → 𝐴 ( 𝐹 ( Inv ‘ 𝑄 ) 𝐺 ) ( 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Inv ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ ( 𝐴 ‘ 𝑦 ) ) ) )
66	8 31 47 48 49 6 65	inviso1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) → 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) )
67	46 66	impbida	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐹 𝐼 𝐺 ) ↔ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )

Metamath Proof Explorer

Theorem fuciso

Proof