Theorem gricer 47376

Description: Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025.)

Assertion

Ref	Expression
gricer	⊢ ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph

Proof of Theorem gricer

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

Step	Hyp	Ref	Expression
1		relinxp 5816	. 2 ⊢ Rel ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))
2		brxp 5727	. . . . 5 ⊢ (𝑔(UHGraph × UHGraph)ℎ ↔ (𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph))
3		gricsym 47373	. . . . . . 7 ⊢ (𝑔 ∈ UHGraph → (𝑔 ≃𝑔𝑟 ℎ → ℎ ≃𝑔𝑟 𝑔))
4	3	adantr 479	. . . . . 6 ⊢ ((𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph) → (𝑔 ≃𝑔𝑟 ℎ → ℎ ≃𝑔𝑟 𝑔))
5		ancom 459	. . . . . . 7 ⊢ ((𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph) ↔ (ℎ ∈ UHGraph ∧ 𝑔 ∈ UHGraph))
6		brxp 5727	. . . . . . 7 ⊢ (ℎ(UHGraph × UHGraph)𝑔 ↔ (ℎ ∈ UHGraph ∧ 𝑔 ∈ UHGraph))
7	5, 6	sylbb2 237	. . . . . 6 ⊢ ((𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph) → ℎ(UHGraph × UHGraph)𝑔)
8	4, 7	jctird 525	. . . . 5 ⊢ ((𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph) → (𝑔 ≃𝑔𝑟 ℎ → (ℎ ≃𝑔𝑟 𝑔 ∧ ℎ(UHGraph × UHGraph)𝑔)))
9	2, 8	sylbi 216	. . . 4 ⊢ (𝑔(UHGraph × UHGraph)ℎ → (𝑔 ≃𝑔𝑟 ℎ → (ℎ ≃𝑔𝑟 𝑔 ∧ ℎ(UHGraph × UHGraph)𝑔)))
10	9	impcom 406	. . 3 ⊢ ((𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ) → (ℎ ≃𝑔𝑟 𝑔 ∧ ℎ(UHGraph × UHGraph)𝑔))
11		brin 5201	. . 3 ⊢ (𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))ℎ ↔ (𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ))
12		brin 5201	. . 3 ⊢ (ℎ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑔 ↔ (ℎ ≃𝑔𝑟 𝑔 ∧ ℎ(UHGraph × UHGraph)𝑔))
13	10, 11, 12	3imtr4i 291	. 2 ⊢ (𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))ℎ → ℎ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑔)
14		grictr 47375	. . . . 5 ⊢ ((𝑔 ≃𝑔𝑟 ℎ ∧ ℎ ≃𝑔𝑟 𝑘) → 𝑔 ≃𝑔𝑟 𝑘)
15	14	ad2ant2r 745	. . . 4 ⊢ (((𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ) ∧ (ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘)) → 𝑔 ≃𝑔𝑟 𝑘)
16		an3 657	. . . . . . . . 9 ⊢ (((𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph) ∧ (ℎ ∈ UHGraph ∧ 𝑘 ∈ UHGraph)) → (𝑔 ∈ UHGraph ∧ 𝑘 ∈ UHGraph))
17	16	ex 411	. . . . . . . 8 ⊢ ((𝑔 ∈ UHGraph ∧ ℎ ∈ UHGraph) → ((ℎ ∈ UHGraph ∧ 𝑘 ∈ UHGraph) → (𝑔 ∈ UHGraph ∧ 𝑘 ∈ UHGraph)))
18		brxp 5727	. . . . . . . . 9 ⊢ (ℎ(UHGraph × UHGraph)𝑘 ↔ (ℎ ∈ UHGraph ∧ 𝑘 ∈ UHGraph))
19		brxp 5727	. . . . . . . . 9 ⊢ (𝑔(UHGraph × UHGraph)𝑘 ↔ (𝑔 ∈ UHGraph ∧ 𝑘 ∈ UHGraph))
20	18, 19	imbi12i 349	. . . . . . . 8 ⊢ ((ℎ(UHGraph × UHGraph)𝑘 → 𝑔(UHGraph × UHGraph)𝑘) ↔ ((ℎ ∈ UHGraph ∧ 𝑘 ∈ UHGraph) → (𝑔 ∈ UHGraph ∧ 𝑘 ∈ UHGraph)))
21	17, 2, 20	3imtr4i 291	. . . . . . 7 ⊢ (𝑔(UHGraph × UHGraph)ℎ → (ℎ(UHGraph × UHGraph)𝑘 → 𝑔(UHGraph × UHGraph)𝑘))
22	21	adantld 489	. . . . . 6 ⊢ (𝑔(UHGraph × UHGraph)ℎ → ((ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘) → 𝑔(UHGraph × UHGraph)𝑘))
23	22	adantl 480	. . . . 5 ⊢ ((𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ) → ((ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘) → 𝑔(UHGraph × UHGraph)𝑘))
24	23	imp 405	. . . 4 ⊢ (((𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ) ∧ (ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘)) → 𝑔(UHGraph × UHGraph)𝑘)
25	15, 24	jca 510	. . 3 ⊢ (((𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ) ∧ (ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘)) → (𝑔 ≃𝑔𝑟 𝑘 ∧ 𝑔(UHGraph × UHGraph)𝑘))
26		brin 5201	. . . 4 ⊢ (ℎ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑘 ↔ (ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘))
27	11, 26	anbi12i 626	. . 3 ⊢ ((𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))ℎ ∧ ℎ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑘) ↔ ((𝑔 ≃𝑔𝑟 ℎ ∧ 𝑔(UHGraph × UHGraph)ℎ) ∧ (ℎ ≃𝑔𝑟 𝑘 ∧ ℎ(UHGraph × UHGraph)𝑘)))
28		brin 5201	. . 3 ⊢ (𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑘 ↔ (𝑔 ≃𝑔𝑟 𝑘 ∧ 𝑔(UHGraph × UHGraph)𝑘))
29	25, 27, 28	3imtr4i 291	. 2 ⊢ ((𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))ℎ ∧ ℎ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑘) → 𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑘)
30		gricref 47372	. . . . 5 ⊢ (𝑔 ∈ UHGraph → 𝑔 ≃𝑔𝑟 𝑔)
31		id 22	. . . . . 6 ⊢ (𝑔 ∈ UHGraph → 𝑔 ∈ UHGraph)
32		brxp 5727	. . . . . 6 ⊢ (𝑔(UHGraph × UHGraph)𝑔 ↔ (𝑔 ∈ UHGraph ∧ 𝑔 ∈ UHGraph))
33	31, 31, 32	sylanbrc 581	. . . . 5 ⊢ (𝑔 ∈ UHGraph → 𝑔(UHGraph × UHGraph)𝑔)
34	30, 33	jca 510	. . . 4 ⊢ (𝑔 ∈ UHGraph → (𝑔 ≃𝑔𝑟 𝑔 ∧ 𝑔(UHGraph × UHGraph)𝑔))
35	32	simplbi 496	. . . . 5 ⊢ (𝑔(UHGraph × UHGraph)𝑔 → 𝑔 ∈ UHGraph)
36	35	adantl 480	. . . 4 ⊢ ((𝑔 ≃𝑔𝑟 𝑔 ∧ 𝑔(UHGraph × UHGraph)𝑔) → 𝑔 ∈ UHGraph)
37	34, 36	impbii 208	. . 3 ⊢ (𝑔 ∈ UHGraph ↔ (𝑔 ≃𝑔𝑟 𝑔 ∧ 𝑔(UHGraph × UHGraph)𝑔))
38		brin 5201	. . 3 ⊢ (𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑔 ↔ (𝑔 ≃𝑔𝑟 𝑔 ∧ 𝑔(UHGraph × UHGraph)𝑔))
39	37, 38	bitr4i 277	. 2 ⊢ (𝑔 ∈ UHGraph ↔ 𝑔( ≃𝑔𝑟 ∩ (UHGraph × UHGraph))𝑔)
40	1, 13, 29, 39	iseri 8752	1 ⊢ ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   ∩ cin 3943   class class class wbr 5149   × cxp 5676   Er wer 8722  UHGraphcuhgr 28941   ≃_𝑔𝑟 cgric 47346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-1o 8487  df-er 8725  df-map 8847  df-uhgr 28943  df-grim 47348  df-gric 47351

This theorem is referenced by: (None)