| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rng2idlring.r | . . 3
⊢ (𝜑 → 𝑅 ∈ Rng) | 
| 2 |  | rng2idlring.i | . . 3
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) | 
| 3 |  | rng2idlring.j | . . 3
⊢ 𝐽 = (𝑅 ↾s 𝐼) | 
| 4 |  | rng2idlring.u | . . 3
⊢ (𝜑 → 𝐽 ∈ Ring) | 
| 5 |  | rng2idlring.b | . . 3
⊢ 𝐵 = (Base‘𝑅) | 
| 6 |  | rng2idlring.t | . . 3
⊢  · =
(.r‘𝑅) | 
| 7 |  | rng2idlring.1 | . . 3
⊢  1 =
(1r‘𝐽) | 
| 8 |  | rngqiprngim.g | . . 3
⊢  ∼ =
(𝑅 ~QG
𝐼) | 
| 9 |  | rngqiprngim.q | . . 3
⊢ 𝑄 = (𝑅 /s ∼ ) | 
| 10 |  | rngqiprngim.c | . . 3
⊢ 𝐶 = (Base‘𝑄) | 
| 11 |  | rngqiprngim.p | . . 3
⊢ 𝑃 = (𝑄 ×s 𝐽) | 
| 12 |  | rngqiprngim.f | . . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈[𝑥] ∼ , ( 1 · 𝑥)〉) | 
| 13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | rngqiprngimf 21308 | . 2
⊢ (𝜑 → 𝐹:𝐵⟶(𝐶 × 𝐼)) | 
| 14 |  | elxpi 5706 | . . . . 5
⊢ (𝑏 ∈ (𝐶 × 𝐼) → ∃𝑝∃𝑞(𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼))) | 
| 15 | 10 | eleq2i 2832 | . . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐶 ↔ 𝑝 ∈ (Base‘𝑄)) | 
| 16 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑝 ∈ V | 
| 17 | 8, 9, 5 | quselbas 19203 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Rng ∧ 𝑝 ∈ V) → (𝑝 ∈ (Base‘𝑄) ↔ ∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ )) | 
| 18 | 1, 16, 17 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↔ ∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ )) | 
| 19 | 15, 18 | bitrid 283 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑝 ∈ 𝐶 ↔ ∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ )) | 
| 20 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 21 |  | rnggrp 20156 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) | 
| 22 | 1, 21 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 23 | 22 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑅 ∈ Grp) | 
| 24 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) | 
| 25 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑅 ∈ Rng) | 
| 26 | 1, 2, 3, 4, 5, 6, 7 | rngqiprng1elbas 21297 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈ 𝐵) | 
| 27 | 26 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 1 ∈ 𝐵) | 
| 28 | 5, 6 | rngcl 20162 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ 𝐵) | 
| 29 | 25, 27, 24, 28 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ 𝐵) | 
| 30 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(-g‘𝑅) = (-g‘𝑅) | 
| 31 | 5, 30 | grpsubcl 19039 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Grp ∧ 𝑐 ∈ 𝐵 ∧ ( 1 · 𝑐) ∈ 𝐵) → (𝑐(-g‘𝑅)( 1 · 𝑐)) ∈ 𝐵) | 
| 32 | 23, 24, 29, 31 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑐(-g‘𝑅)( 1 · 𝑐)) ∈ 𝐵) | 
| 33 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) | 
| 34 | 5, 33 | 2idlss 21273 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ (2Ideal‘𝑅) → 𝐼 ⊆ 𝐵) | 
| 35 | 2, 34 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐼 ⊆ 𝐵) | 
| 36 | 35 | sselda 3982 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼) → 𝑞 ∈ 𝐵) | 
| 37 | 36 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 ∈ 𝐵) | 
| 38 | 5, 20, 23, 32, 37 | grpcld 18966 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) ∈ 𝐵) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) → ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) ∈ 𝐵) | 
| 40 |  | opeq1 4872 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = [𝑐] ∼ → 〈𝑝, 𝑞〉 = 〈[𝑐] ∼ , 𝑞〉) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) →
〈𝑝, 𝑞〉 = 〈[𝑐] ∼ , 𝑞〉) | 
| 42 |  | eceq1 8785 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) → [𝑎] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ) | 
| 43 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) → ( 1 · 𝑎) = ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))) | 
| 44 | 42, 43 | opeq12d 4880 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) → 〈[𝑎] ∼ , ( 1 · 𝑎)〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉) | 
| 45 | 41, 44 | eqeqan12d 2750 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) ∧ 𝑎 = ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)) → (〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉 ↔ 〈[𝑐] ∼ , 𝑞〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉)) | 
| 46 |  | rngabl 20153 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) | 
| 47 | 1, 46 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑅 ∈ Abel) | 
| 48 | 47 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑅 ∈ Abel) | 
| 49 | 5, 20, 30 | ablsubaddsub 19833 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Abel ∧ (𝑐 ∈ 𝐵 ∧ ( 1 · 𝑐) ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) = (𝑞(-g‘𝑅)( 1 · 𝑐))) | 
| 50 | 48, 24, 29, 37, 49 | syl13anc 1373 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) = (𝑞(-g‘𝑅)( 1 · 𝑐))) | 
| 51 | 4 | ringgrpd 20240 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐽 ∈ Grp) | 
| 52 | 51 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝐽 ∈ Grp) | 
| 53 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Base‘𝐽) =
(Base‘𝐽) | 
| 54 | 2, 3, 53 | 2idlbas 21274 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (Base‘𝐽) = 𝐼) | 
| 55 | 54 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐼 = (Base‘𝐽)) | 
| 56 | 55 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑞 ∈ 𝐼 ↔ 𝑞 ∈ (Base‘𝐽))) | 
| 57 | 56 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼) → 𝑞 ∈ (Base‘𝐽)) | 
| 58 | 57 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 ∈ (Base‘𝐽)) | 
| 59 | 1, 2, 3, 4, 5, 6, 7 | rngqiprngghmlem1 21298 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ (Base‘𝐽)) | 
| 60 | 59 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ (Base‘𝐽)) | 
| 61 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(-g‘𝐽) = (-g‘𝐽) | 
| 62 | 53, 61 | grpsubcl 19039 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 ∈ Grp ∧ 𝑞 ∈ (Base‘𝐽) ∧ ( 1 · 𝑐) ∈ (Base‘𝐽)) → (𝑞(-g‘𝐽)( 1 · 𝑐)) ∈ (Base‘𝐽)) | 
| 63 | 52, 58, 60, 62 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑞(-g‘𝐽)( 1 · 𝑐)) ∈ (Base‘𝐽)) | 
| 64 |  | ringrng 20283 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) | 
| 65 | 4, 64 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐽 ∈ Rng) | 
| 66 | 3, 65 | eqeltrrid 2845 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) | 
| 67 | 1, 2, 66 | rng2idlnsg 21277 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) | 
| 68 |  | nsgsubg 19177 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 70 | 69 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝐼 ∈ (SubGrp‘𝑅)) | 
| 71 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 ∈ 𝐼) | 
| 72 | 54 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (Base‘𝐽) = 𝐼) | 
| 73 | 60, 72 | eleqtrd 2842 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · 𝑐) ∈ 𝐼) | 
| 74 | 30, 3, 61 | subgsub 19157 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈ (SubGrp‘𝑅) ∧ 𝑞 ∈ 𝐼 ∧ ( 1 · 𝑐) ∈ 𝐼) → (𝑞(-g‘𝑅)( 1 · 𝑐)) = (𝑞(-g‘𝐽)( 1 · 𝑐))) | 
| 75 | 70, 71, 73, 74 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑞(-g‘𝑅)( 1 · 𝑐)) = (𝑞(-g‘𝐽)( 1 · 𝑐))) | 
| 76 | 55 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝐼 = (Base‘𝐽)) | 
| 77 | 63, 75, 76 | 3eltr4d 2855 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (𝑞(-g‘𝑅)( 1 · 𝑐)) ∈ 𝐼) | 
| 78 | 50, 77 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) ∈ 𝐼) | 
| 79 | 5, 30, 8 | qusecsub 19854 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Abel ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ (𝑐 ∈ 𝐵 ∧ ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞) ∈ 𝐵)) → ([𝑐] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ↔ (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) ∈ 𝐼)) | 
| 80 | 48, 70, 24, 38, 79 | syl22anc 838 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ([𝑐] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ↔ (((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)(-g‘𝑅)𝑐) ∈ 𝐼)) | 
| 81 | 78, 80 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → [𝑐] ∼ = [((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ ) | 
| 82 | 1, 2, 3, 4, 5, 6, 7 | rngqiprngimfolem 21301 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼 ∧ 𝑐 ∈ 𝐵) → ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)) = 𝑞) | 
| 83 | 82 | 3expa 1118 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)) = 𝑞) | 
| 84 | 83 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 𝑞 = ( 1 · ((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))) | 
| 85 | 81, 84 | opeq12d 4880 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) → 〈[𝑐] ∼ , 𝑞〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉) | 
| 86 | 85 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) →
〈[𝑐] ∼ ,
𝑞〉 = 〈[((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞)] ∼ , ( 1 ·
((𝑐(-g‘𝑅)( 1 · 𝑐))(+g‘𝑅)𝑞))〉) | 
| 87 | 39, 45, 86 | rspcedvd 3623 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑞 ∈ 𝐼) ∧ 𝑐 ∈ 𝐵) ∧ 𝑝 = [𝑐] ∼ ) →
∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) | 
| 88 | 87 | rexlimdva2 3156 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐼) → (∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) | 
| 89 | 88 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑞 ∈ 𝐼 → (∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉))) | 
| 90 | 89 | com23 86 | . . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑐 ∈ 𝐵 𝑝 = [𝑐] ∼ → (𝑞 ∈ 𝐼 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉))) | 
| 91 | 19, 90 | sylbid 240 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑝 ∈ 𝐶 → (𝑞 ∈ 𝐼 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉))) | 
| 92 | 91 | impd 410 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼) → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) | 
| 93 | 92 | com12 32 | . . . . . . . . . 10
⊢ ((𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼) → (𝜑 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) | 
| 94 | 93 | adantl 481 | . . . . . . . . 9
⊢ ((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) → (𝜑 → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) | 
| 95 | 94 | imp 406 | . . . . . . . 8
⊢ (((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) → ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) | 
| 96 |  | simplll 774 | . . . . . . . . . 10
⊢ ((((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) ∧ 𝑎 ∈ 𝐵) → 𝑏 = 〈𝑝, 𝑞〉) | 
| 97 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | rngqiprngimfv 21309 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) | 
| 98 | 97 | adantll 714 | . . . . . . . . . 10
⊢ ((((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) | 
| 99 | 96, 98 | eqeq12d 2752 | . . . . . . . . 9
⊢ ((((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) ∧ 𝑎 ∈ 𝐵) → (𝑏 = (𝐹‘𝑎) ↔ 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) | 
| 100 | 99 | rexbidva 3176 | . . . . . . . 8
⊢ (((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) → (∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎) ↔ ∃𝑎 ∈ 𝐵 〈𝑝, 𝑞〉 = 〈[𝑎] ∼ , ( 1 · 𝑎)〉)) | 
| 101 | 95, 100 | mpbird 257 | . . . . . . 7
⊢ (((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) ∧ 𝜑) → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎)) | 
| 102 | 101 | ex 412 | . . . . . 6
⊢ ((𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) → (𝜑 → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) | 
| 103 | 102 | exlimivv 1931 | . . . . 5
⊢
(∃𝑝∃𝑞(𝑏 = 〈𝑝, 𝑞〉 ∧ (𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼)) → (𝜑 → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) | 
| 104 | 14, 103 | syl 17 | . . . 4
⊢ (𝑏 ∈ (𝐶 × 𝐼) → (𝜑 → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) | 
| 105 | 104 | impcom 407 | . . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐶 × 𝐼)) → ∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎)) | 
| 106 | 105 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑏 ∈ (𝐶 × 𝐼)∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎)) | 
| 107 |  | dffo3 7121 | . 2
⊢ (𝐹:𝐵–onto→(𝐶 × 𝐼) ↔ (𝐹:𝐵⟶(𝐶 × 𝐼) ∧ ∀𝑏 ∈ (𝐶 × 𝐼)∃𝑎 ∈ 𝐵 𝑏 = (𝐹‘𝑎))) | 
| 108 | 13, 106, 107 | sylanbrc 583 | 1
⊢ (𝜑 → 𝐹:𝐵–onto→(𝐶 × 𝐼)) |