Theorem hashfacen 11300

Description: The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)

Assertion

Ref	Expression
hashfacen	⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝐶,𝑓   𝐷,𝑓

Proof of Theorem hashfacen

Dummy variables 𝑔 ℎ 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bren 7030	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑔 𝑔:𝐴–1-1-onto→𝐵)
2		bren 7030	. 2 ⊢ (𝐶 ≈ 𝐷 ↔ ∃ℎ ℎ:𝐶–1-1-onto→𝐷)
3		eeanv 1992	. . 3 ⊢ (∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ↔ (∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷))
4		f1odm 5643	. . . . . . . 8 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → dom ℎ = 𝐶)
5		vex 2824	. . . . . . . . 9 ⊢ ℎ ∈ V
6	5	dmex 5049	. . . . . . . 8 ⊢ dom ℎ ∈ V
7	4, 6	eqeltrrdi 2330	. . . . . . 7 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐶 ∈ V)
8		f1odm 5643	. . . . . . . 8 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → dom 𝑔 = 𝐴)
9		vex 2824	. . . . . . . . 9 ⊢ 𝑔 ∈ V
10	9	dmex 5049	. . . . . . . 8 ⊢ dom 𝑔 ∈ V
11	8, 10	eqeltrrdi 2330	. . . . . . 7 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
12		fnmap 6929	. . . . . . . 8 ⊢ ↑𝑚 Fn (V × V)
13		fnovex 6118	. . . . . . . 8 ⊢ (( ↑𝑚 Fn (V × V) ∧ 𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 ↑𝑚 𝐴) ∈ V)
14	12, 13	mp3an1 1365	. . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 ↑𝑚 𝐴) ∈ V)
15	7, 11, 14	syl2anr 290	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝐶 ↑𝑚 𝐴) ∈ V)
16		f1of 5639	. . . . . . . 8 ⊢ (𝑓:𝐴–1-1-onto→𝐶 → 𝑓:𝐴⟶𝐶)
17		elmapg 6935	. . . . . . . . 9 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝑓 ∈ (𝐶 ↑𝑚 𝐴) ↔ 𝑓:𝐴⟶𝐶))
18	7, 11, 17	syl2anr 290	. . . . . . . 8 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐶 ↑𝑚 𝐴) ↔ 𝑓:𝐴⟶𝐶))
19	16, 18	imbitrrid 156	. . . . . . 7 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐴–1-1-onto→𝐶 → 𝑓 ∈ (𝐶 ↑𝑚 𝐴)))
20	19	abssdv 3322	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ⊆ (𝐶 ↑𝑚 𝐴))
21	15, 20	ssexd 4273	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∈ V)
22		f1ofo 5646	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–onto→𝐷)
23		forn 5618	. . . . . . . . 9 ⊢ (ℎ:𝐶–onto→𝐷 → ran ℎ = 𝐷)
24	22, 23	syl 14	. . . . . . . 8 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ran ℎ = 𝐷)
25	5	rnex 5050	. . . . . . . 8 ⊢ ran ℎ ∈ V
26	24, 25	eqeltrrdi 2330	. . . . . . 7 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → 𝐷 ∈ V)
27		f1ofo 5646	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝑔:𝐴–onto→𝐵)
28		forn 5618	. . . . . . . . 9 ⊢ (𝑔:𝐴–onto→𝐵 → ran 𝑔 = 𝐵)
29	27, 28	syl 14	. . . . . . . 8 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → ran 𝑔 = 𝐵)
30	9	rnex 5050	. . . . . . . 8 ⊢ ran 𝑔 ∈ V
31	29, 30	eqeltrrdi 2330	. . . . . . 7 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
32		fnovex 6118	. . . . . . . 8 ⊢ (( ↑𝑚 Fn (V × V) ∧ 𝐷 ∈ V ∧ 𝐵 ∈ V) → (𝐷 ↑𝑚 𝐵) ∈ V)
33	12, 32	mp3an1 1365	. . . . . . 7 ⊢ ((𝐷 ∈ V ∧ 𝐵 ∈ V) → (𝐷 ↑𝑚 𝐵) ∈ V)
34	26, 31, 33	syl2anr 290	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝐷 ↑𝑚 𝐵) ∈ V)
35		f1of 5639	. . . . . . . 8 ⊢ (𝑓:𝐵–1-1-onto→𝐷 → 𝑓:𝐵⟶𝐷)
36		elmapg 6935	. . . . . . . . 9 ⊢ ((𝐷 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ (𝐷 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝐷))
37	26, 31, 36	syl2anr 290	. . . . . . . 8 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓 ∈ (𝐷 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝐷))
38	35, 37	imbitrrid 156	. . . . . . 7 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑓:𝐵–1-1-onto→𝐷 → 𝑓 ∈ (𝐷 ↑𝑚 𝐵)))
39	38	abssdv 3322	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ⊆ (𝐷 ↑𝑚 𝐵))
40	34, 39	ssexd 4273	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ∈ V)
41		f1oco 5662	. . . . . . . . 9 ⊢ ((ℎ:𝐶–1-1-onto→𝐷 ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
42	41	adantll 480	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
43		f1ocnv 5652	. . . . . . . . 9 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → ◡𝑔:𝐵–1-1-onto→𝐴)
44	43	ad2antrr 492	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ◡𝑔:𝐵–1-1-onto→𝐴)
45		f1oco 5662	. . . . . . . 8 ⊢ (((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 ∧ ◡𝑔:𝐵–1-1-onto→𝐴) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
46	42, 44, 45	syl2anc 415	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑥:𝐴–1-1-onto→𝐶) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
47	46	ex 115	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥:𝐴–1-1-onto→𝐶 → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷))
48		vex 2824	. . . . . . 7 ⊢ 𝑥 ∈ V
49		f1oeq1 5627	. . . . . . 7 ⊢ (𝑓 = 𝑥 → (𝑓:𝐴–1-1-onto→𝐶 ↔ 𝑥:𝐴–1-1-onto→𝐶))
50	48, 49	elab 2970	. . . . . 6 ⊢ (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ 𝑥:𝐴–1-1-onto→𝐶)
51	5, 48	coex 5333	. . . . . . . 8 ⊢ (ℎ ∘ 𝑥) ∈ V
52	9	cnvex 5326	. . . . . . . 8 ⊢ ◡𝑔 ∈ V
53	51, 52	coex 5333	. . . . . . 7 ⊢ ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ V
54		f1oeq1 5627	. . . . . . 7 ⊢ (𝑓 = ((ℎ ∘ 𝑥) ∘ ◡𝑔) → (𝑓:𝐵–1-1-onto→𝐷 ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷))
55	53, 54	elab 2970	. . . . . 6 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
56	47, 50, 55	3imtr4g 205	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} → ((ℎ ∘ 𝑥) ∘ ◡𝑔) ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}))
57		f1ocnv 5652	. . . . . . . . 9 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ◡ℎ:𝐷–1-1-onto→𝐶)
58	57	ad2antlr 493	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → ◡ℎ:𝐷–1-1-onto→𝐶)
59		f1oco 5662	. . . . . . . . . 10 ⊢ ((𝑦:𝐵–1-1-onto→𝐷 ∧ 𝑔:𝐴–1-1-onto→𝐵) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
60	59	ancoms 268	. . . . . . . . 9 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
61	60	adantlr 481	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
62		f1oco 5662	. . . . . . . 8 ⊢ ((◡ℎ:𝐷–1-1-onto→𝐶 ∧ (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
63	58, 61, 62	syl2anc 415	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ 𝑦:𝐵–1-1-onto→𝐷) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
64	63	ex 115	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦:𝐵–1-1-onto→𝐷 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶))
65		vex 2824	. . . . . . 7 ⊢ 𝑦 ∈ V
66		f1oeq1 5627	. . . . . . 7 ⊢ (𝑓 = 𝑦 → (𝑓:𝐵–1-1-onto→𝐷 ↔ 𝑦:𝐵–1-1-onto→𝐷))
67	65, 66	elab 2970	. . . . . 6 ⊢ (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} ↔ 𝑦:𝐵–1-1-onto→𝐷)
68	5	cnvex 5326	. . . . . . . 8 ⊢ ◡ℎ ∈ V
69	65, 9	coex 5333	. . . . . . . 8 ⊢ (𝑦 ∘ 𝑔) ∈ V
70	68, 69	coex 5333	. . . . . . 7 ⊢ (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ V
71		f1oeq1 5627	. . . . . . 7 ⊢ (𝑓 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) → (𝑓:𝐴–1-1-onto→𝐶 ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶))
72	70, 71	elab 2970	. . . . . 6 ⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ↔ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
73	64, 67, 72	3imtr4g 205	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → (𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷} → (◡ℎ ∘ (𝑦 ∘ 𝑔)) ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶}))
74	50, 67	anbi12i 464	. . . . . 6 ⊢ ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) ↔ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷))
75		coass 5306	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔))
76		f1ococnv1 5668	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝐴–1-1-onto→𝐵 → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴))
77	76	ad2antrr 492	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡𝑔 ∘ 𝑔) = ( I ↾ 𝐴))
78	77	coeq2d 4942	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)))
79	42	adantrr 483	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷)
80		f1of 5639	. . . . . . . . . . . . 13 ⊢ ((ℎ ∘ 𝑥):𝐴–1-1-onto→𝐷 → (ℎ ∘ 𝑥):𝐴⟶𝐷)
81		fcoi1 5572	. . . . . . . . . . . . 13 ⊢ ((ℎ ∘ 𝑥):𝐴⟶𝐷 → ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)) = (ℎ ∘ 𝑥))
82	79, 80, 81	3syl 17	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ( I ↾ 𝐴)) = (ℎ ∘ 𝑥))
83	78, 82	eqtrd 2271	. . . . . . . . . . 11 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ (◡𝑔 ∘ 𝑔)) = (ℎ ∘ 𝑥))
84	75, 83	eqtr2id 2284	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ 𝑥) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))
85		coass 5306	. . . . . . . . . . 11 ⊢ ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔)))
86		f1ococnv2 5666	. . . . . . . . . . . . . 14 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷))
87	86	ad2antlr 493	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ ◡ℎ) = ( I ↾ 𝐷))
88	87	coeq1d 4941	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)))
89	61	adantrl 482	. . . . . . . . . . . . 13 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷)
90		f1of 5639	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∘ 𝑔):𝐴–1-1-onto→𝐷 → (𝑦 ∘ 𝑔):𝐴⟶𝐷)
91		fcoi2 5573	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∘ 𝑔):𝐴⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
92	89, 90, 91	3syl 17	. . . . . . . . . . . 12 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (( I ↾ 𝐷) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
93	88, 92	eqtrd 2271	. . . . . . . . . . 11 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ ◡ℎ) ∘ (𝑦 ∘ 𝑔)) = (𝑦 ∘ 𝑔))
94	85, 93	eqtr3id 2285	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) = (𝑦 ∘ 𝑔))
95	84, 94	eqeq12d 2253	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔)))
96		eqcom 2240	. . . . . . . . 9 ⊢ ((((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) = (𝑦 ∘ 𝑔) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔))
97	95, 96	bitrdi 196	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ (𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔)))
98		f1of1 5638	. . . . . . . . . 10 ⊢ (ℎ:𝐶–1-1-onto→𝐷 → ℎ:𝐶–1-1→𝐷)
99	98	ad2antlr 493	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ℎ:𝐶–1-1→𝐷)
100		f1of 5639	. . . . . . . . . 10 ⊢ (𝑥:𝐴–1-1-onto→𝐶 → 𝑥:𝐴⟶𝐶)
101	100	ad2antrl 494	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑥:𝐴⟶𝐶)
102	63	adantrl 482	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶)
103		f1of 5639	. . . . . . . . . 10 ⊢ ((◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴–1-1-onto→𝐶 → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶)
104	102, 103	syl 14	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶)
105		cocan1 5993	. . . . . . . . 9 ⊢ ((ℎ:𝐶–1-1→𝐷 ∧ 𝑥:𝐴⟶𝐶 ∧ (◡ℎ ∘ (𝑦 ∘ 𝑔)):𝐴⟶𝐶) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔))))
106	99, 101, 104, 105	syl3anc 1278	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) = (ℎ ∘ (◡ℎ ∘ (𝑦 ∘ 𝑔))) ↔ 𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔))))
107	27	ad2antrr 492	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑔:𝐴–onto→𝐵)
108		f1ofn 5640	. . . . . . . . . 10 ⊢ (𝑦:𝐵–1-1-onto→𝐷 → 𝑦 Fn 𝐵)
109	108	ad2antll 495	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → 𝑦 Fn 𝐵)
110	46	adantrr 483	. . . . . . . . . 10 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷)
111		f1ofn 5640	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝑥) ∘ ◡𝑔):𝐵–1-1-onto→𝐷 → ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵)
112	110, 111	syl 14	. . . . . . . . 9 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵)
113		cocan2 5994	. . . . . . . . 9 ⊢ ((𝑔:𝐴–onto→𝐵 ∧ 𝑦 Fn 𝐵 ∧ ((ℎ ∘ 𝑥) ∘ ◡𝑔) Fn 𝐵) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
114	107, 109, 112, 113	syl3anc 1278	. . . . . . . 8 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → ((𝑦 ∘ 𝑔) = (((ℎ ∘ 𝑥) ∘ ◡𝑔) ∘ 𝑔) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
115	97, 106, 114	3bitr3d 218	. . . . . . 7 ⊢ (((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) ∧ (𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷)) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔)))
116	115	ex 115	. . . . . 6 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))))
117	74, 116	biimtrid 152	. . . . 5 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → ((𝑥 ∈ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ∧ 𝑦 ∈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) → (𝑥 = (◡ℎ ∘ (𝑦 ∘ 𝑔)) ↔ 𝑦 = ((ℎ ∘ 𝑥) ∘ ◡𝑔))))
118	21, 40, 56, 73, 117	en3d 7055	. . . 4 ⊢ ((𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
119	118	exlimivv 1952	. . 3 ⊢ (∃𝑔∃ℎ(𝑔:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
120	3, 119	sylbir 135	. 2 ⊢ ((∃𝑔 𝑔:𝐴–1-1-onto→𝐵 ∧ ∃ℎ ℎ:𝐶–1-1-onto→𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
121	1, 2, 120	syl2anb 291	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209  {cab 2224  Vcvv 2821   class class class wbr 4130   I cid 4433   × cxp 4772  ^◡ccnv 4773  dom cdm 4774  ran crn 4775   ↾ cres 4776   ∘ ccom 4778   Fn wfn 5372  ⟶wf 5373  –1-1→wf1 5374  –onto→wfo 5375  –1-1-onto→wf1o 5376  (class class class)co 6085   ↑_𝑚 cmap 6922   ≈ cen 7020

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-map 6924  df-en 7023

This theorem is used by: (None)