invpropdlem

	Ref	Expression
Hypotheses	sectpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	sectpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
Assertion	invpropdlem	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝑃 ∈ ( Inv ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
2		sectpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
3		simpr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝑃 ∈ ( Inv ‘ 𝐶 ) )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
6		df-inv	⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
7	6	mptrcl	⊢ ( 𝑃 ∈ ( Inv ‘ 𝐶 ) → 𝐶 ∈ Cat )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
9		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
10	4 5 8 9	invffval	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
11		df-mpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) }
12	10 11	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( Inv ‘ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) } )
13	3 12	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝑃 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) } )
14		eloprab1st2nd	⊢ ( 𝑃 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) } → 𝑃 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ )
15	13 14	syl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝑃 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ )
16	1	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
17	2	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
18	16 17	sectpropd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐷 ) )
19	18	oveqd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) )
20	18	oveqd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
21	20	cnveqd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
22	19 21	ineq12d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
23		eleq1	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) )
24	23	anbi1d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) )
25		oveq1	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) )
26		oveq2	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) = ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
27	26	cnveqd	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) = ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
28	25 27	ineq12d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
29	28	eqeq2d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ↔ 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) )
30	24 29	anbi12d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) ) )
31		eleq1	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) )
32	31	anbi2d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ) )
33		oveq2	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) )
34		oveq1	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
35	34	cnveqd	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
36	33 35	ineq12d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
37	36	eqeq2d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ↔ 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) )
38	32 37	anbi12d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) ) )
39		eqeq1	⊢ ( 𝑧 = ( 2^nd ‘ 𝑃 ) → ( 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ↔ ( 2^nd ‘ 𝑃 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) )
40	39	anbi2d	⊢ ( 𝑧 = ( 2^nd ‘ 𝑃 ) → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ∧ ( 2^nd ‘ 𝑃 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) ) )
41	30 38 40	eloprabi	⊢ ( 𝑃 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) } → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ∧ ( 2^nd ‘ 𝑃 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) )
42	13 41	syl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ∧ ( 2^nd ‘ 𝑃 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) )
43	42	simprd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( 2^nd ‘ 𝑃 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
44		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
45		eqid	⊢ ( Inv ‘ 𝐷 ) = ( Inv ‘ 𝐷 )
46	42	simplld	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) )
47	16	homfeqbas	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
48	46 47	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐷 ) )
49	48	elfvexd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝐷 ∈ V )
50	16 17 8 49	catpropd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
51	8 50	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
52	42	simplrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) )
53	52 47	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐷 ) )
54		eqid	⊢ ( Sect ‘ 𝐷 ) = ( Sect ‘ 𝐷 )
55	44 45 51 48 53 54	invfval	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Inv ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∩ ^◡ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
56	22 43 55	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Inv ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( 2^nd ‘ 𝑃 ) )
57		invfn	⊢ ( 𝐷 ∈ Cat → ( Inv ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
58	51 57	syl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( Inv ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
59		fnbrovb	⊢ ( ( ( Inv ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Inv ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( 2^nd ‘ 𝑃 ) ↔ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ ( Inv ‘ 𝐷 ) ( 2^nd ‘ 𝑃 ) ) )
60	58 48 53 59	syl12anc	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Inv ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( 2^nd ‘ 𝑃 ) ↔ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ ( Inv ‘ 𝐷 ) ( 2^nd ‘ 𝑃 ) ) )
61	56 60	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ ( Inv ‘ 𝐷 ) ( 2^nd ‘ 𝑃 ) )
62		df-br	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ ( Inv ‘ 𝐷 ) ( 2^nd ‘ 𝑃 ) ↔ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ ∈ ( Inv ‘ 𝐷 ) )
63	61 62	sylib	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ ∈ ( Inv ‘ 𝐷 ) )
64	15 63	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Inv ‘ 𝐶 ) ) → 𝑃 ∈ ( Inv ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem invpropdlem

Proof