isopropdlem

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

Proof

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

Metamath Proof Explorer

Theorem isopropdlem

Proof