Metamath Proof Explorer

Theorem rngqiprngimfo

Description: F is a function from (the base set of) a non-unital ring onto the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 5-Mar-2025) (Proof shortened by AV, 24-Mar-2025)

Ref Expression
Hypotheses rng2idlring.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rng2idlring.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
rng2idlring.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
rng2idlring.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
rng2idlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rng2idlring.t ⊢ · = ( .r ‘ 𝑅 )
rng2idlring.1 ⊢ 1 = ( 1r ‘ 𝐽 )
rngqiprngim.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
rngqiprngim.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
rngqiprngim.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
rngqiprngim.p ⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
rngqiprngim.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
Assertion rngqiprngimfo ( 𝜑 → 𝐹 : 𝐵 –onto→ ( 𝐶 × 𝐼 ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
2 rng2idlring.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3 rng2idlring.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 rng2idlring.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
5 rng2idlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 rng2idlring.t ⊢ · = ( .r ‘ 𝑅 )
7 rng2idlring.1 ⊢ 1 = ( 1r ‘ 𝐽 )
8 rngqiprngim.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9 rngqiprngim.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
10 rngqiprngim.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
11 rngqiprngim.p ⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
12 rngqiprngim.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
13 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimf ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 𝐶 × 𝐼 ) )
14 elxpi ⊢ ( 𝑏 ∈ ( 𝐶 × 𝐼 ) → ∃ 𝑝 ∃ 𝑞 ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) )
15 10 eleq2i ⊢ ( 𝑝 ∈ 𝐶 ↔ 𝑝 ∈ ( Base ‘ 𝑄 ) )
16 vex ⊢ 𝑝 ∈ V
17 8 9 5 quselbas ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑝 ∈ V ) → ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↔ ∃ 𝑐 ∈ 𝐵 𝑝 = [ 𝑐 ] ∼ ) )
18 1 16 17 sylancl ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↔ ∃ 𝑐 ∈ 𝐵 𝑝 = [ 𝑐 ] ∼ ) )
19 15 18 bitrid ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐶 ↔ ∃ 𝑐 ∈ 𝐵 𝑝 = [ 𝑐 ] ∼ ) )
20 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
21 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
22 1 21 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑅 ∈ Grp )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ 𝐵 )
25 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑅 ∈ Rng )
26 1 2 3 4 5 6 7 rngqiprng1elbas ⊢ ( 𝜑 → 1 ∈ 𝐵 )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 1 ∈ 𝐵 )
28 5 6 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 1 · 𝑐 ) ∈ 𝐵 )
29 25 27 24 28 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 1 · 𝑐 ) ∈ 𝐵 )
30 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
31 5 30 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑐 ∈ 𝐵 ∧ ( 1 · 𝑐 ) ∈ 𝐵 ) → ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ∈ 𝐵 )
32 23 24 29 31 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ∈ 𝐵 )
33 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
34 5 33 2idlss ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
35 2 34 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
36 35 sselda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) → 𝑞 ∈ 𝐵 )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑞 ∈ 𝐵 )
38 5 20 23 32 37 grpcld ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ∈ 𝐵 )
39 38 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑝 = [ 𝑐 ] ∼ ) → ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ∈ 𝐵 )
40 opeq1 ⊢ ( 𝑝 = [ 𝑐 ] ∼ → ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑐 ] ∼ , 𝑞 ⟩ )
41 40 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑝 = [ 𝑐 ] ∼ ) → ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑐 ] ∼ , 𝑞 ⟩ )
42 eceq1 ⊢ ( 𝑎 = ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) → [ 𝑎 ] ∼ = [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ )
43 oveq2 ⊢ ( 𝑎 = ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) → ( 1 · 𝑎 ) = ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) )
44 42 43 opeq12d ⊢ ( 𝑎 = ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) → ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ = ⟨ [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ , ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ )
45 41 44 eqeqan12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑝 = [ 𝑐 ] ∼ ) ∧ 𝑎 = ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) → ( ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ↔ ⟨ [ 𝑐 ] ∼ , 𝑞 ⟩ = ⟨ [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ , ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ ) )
46 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
47 1 46 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑅 ∈ Abel )
49 5 20 30 ablsubaddsub ⊢ ( ( 𝑅 ∈ Abel ∧ ( 𝑐 ∈ 𝐵 ∧ ( 1 · 𝑐 ) ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ( -g ‘ 𝑅 ) 𝑐 ) = ( 𝑞 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) )
50 48 24 29 37 49 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ( -g ‘ 𝑅 ) 𝑐 ) = ( 𝑞 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) )
51 4 ringgrpd ⊢ ( 𝜑 → 𝐽 ∈ Grp )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐽 ∈ Grp )
53 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
54 2 3 53 2idlbas ⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = 𝐼 )
55 54 eqcomd ⊢ ( 𝜑 → 𝐼 = ( Base ‘ 𝐽 ) )
56 55 eleq2d ⊢ ( 𝜑 → ( 𝑞 ∈ 𝐼 ↔ 𝑞 ∈ ( Base ‘ 𝐽 ) ) )
57 56 biimpa ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) → 𝑞 ∈ ( Base ‘ 𝐽 ) )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑞 ∈ ( Base ‘ 𝐽 ) )
59 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ) → ( 1 · 𝑐 ) ∈ ( Base ‘ 𝐽 ) )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 1 · 𝑐 ) ∈ ( Base ‘ 𝐽 ) )
61 eqid ⊢ ( -g ‘ 𝐽 ) = ( -g ‘ 𝐽 )
62 53 61 grpsubcl ⊢ ( ( 𝐽 ∈ Grp ∧ 𝑞 ∈ ( Base ‘ 𝐽 ) ∧ ( 1 · 𝑐 ) ∈ ( Base ‘ 𝐽 ) ) → ( 𝑞 ( -g ‘ 𝐽 ) ( 1 · 𝑐 ) ) ∈ ( Base ‘ 𝐽 ) )
63 52 58 60 62 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑞 ( -g ‘ 𝐽 ) ( 1 · 𝑐 ) ) ∈ ( Base ‘ 𝐽 ) )
64 ringrng ⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
65 4 64 syl ⊢ ( 𝜑 → 𝐽 ∈ Rng )
66 3 65 eqeltrrid ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
67 1 2 66 rng2idlnsg ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
68 nsgsubg ⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
69 67 68 syl ⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
71 simplr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑞 ∈ 𝐼 )
72 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( Base ‘ 𝐽 ) = 𝐼 )
73 60 72 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 1 · 𝑐 ) ∈ 𝐼 )
74 30 3 61 subgsub ⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑞 ∈ 𝐼 ∧ ( 1 · 𝑐 ) ∈ 𝐼 ) → ( 𝑞 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) = ( 𝑞 ( -g ‘ 𝐽 ) ( 1 · 𝑐 ) ) )
75 70 71 73 74 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑞 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) = ( 𝑞 ( -g ‘ 𝐽 ) ( 1 · 𝑐 ) ) )
76 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝐼 = ( Base ‘ 𝐽 ) )
77 63 75 76 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑞 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ∈ 𝐼 )
78 50 77 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐼 )
79 5 30 8 qusecsub ⊢ ( ( ( 𝑅 ∈ Abel ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑐 ∈ 𝐵 ∧ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ∈ 𝐵 ) ) → ( [ 𝑐 ] ∼ = [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ ↔ ( ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐼 ) )
80 48 70 24 38 79 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( [ 𝑐 ] ∼ = [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ ↔ ( ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐼 ) )
81 78 80 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → [ 𝑐 ] ∼ = [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ )
82 1 2 3 4 5 6 7 rngqiprngimfolem ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ∧ 𝑐 ∈ 𝐵 ) → ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) = 𝑞 )
83 82 3expa ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) = 𝑞 )
84 83 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → 𝑞 = ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) )
85 81 84 opeq12d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) → ⟨ [ 𝑐 ] ∼ , 𝑞 ⟩ = ⟨ [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ , ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ )
86 85 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑝 = [ 𝑐 ] ∼ ) → ⟨ [ 𝑐 ] ∼ , 𝑞 ⟩ = ⟨ [ ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ] ∼ , ( 1 · ( ( 𝑐 ( -g ‘ 𝑅 ) ( 1 · 𝑐 ) ) ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ )
87 39 45 86 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) ∧ 𝑐 ∈ 𝐵 ) ∧ 𝑝 = [ 𝑐 ] ∼ ) → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
88 87 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐼 ) → ( ∃ 𝑐 ∈ 𝐵 𝑝 = [ 𝑐 ] ∼ → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) )
89 88 ex ⊢ ( 𝜑 → ( 𝑞 ∈ 𝐼 → ( ∃ 𝑐 ∈ 𝐵 𝑝 = [ 𝑐 ] ∼ → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) ) )
90 89 com23 ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐵 𝑝 = [ 𝑐 ] ∼ → ( 𝑞 ∈ 𝐼 → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) ) )
91 19 90 sylbid ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐶 → ( 𝑞 ∈ 𝐼 → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) ) )
92 91 impd ⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) )
93 92 com12 ⊢ ( ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) → ( 𝜑 → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) )
94 93 adantl ⊢ ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) → ( 𝜑 → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) )
95 94 imp ⊢ ( ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) ∧ 𝜑 ) → ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
96 simplll ⊢ ( ( ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ 𝑎 ∈ 𝐵 ) → 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ )
97 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
98 97 adantll ⊢ ( ( ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
99 96 98 eqeq12d ⊢ ( ( ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 = ( 𝐹 ‘ 𝑎 ) ↔ ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) )
100 99 rexbidva ⊢ ( ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) ∧ 𝜑 ) → ( ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) ↔ ∃ 𝑎 ∈ 𝐵 ⟨ 𝑝 , 𝑞 ⟩ = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ) )
101 95 100 mpbird ⊢ ( ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) ∧ 𝜑 ) → ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) )
102 101 ex ⊢ ( ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) → ( 𝜑 → ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) ) )
103 102 exlimivv ⊢ ( ∃ 𝑝 ∃ 𝑞 ( 𝑏 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐼 ) ) → ( 𝜑 → ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) ) )
104 14 103 syl ⊢ ( 𝑏 ∈ ( 𝐶 × 𝐼 ) → ( 𝜑 → ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) ) )
105 104 impcom ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐶 × 𝐼 ) ) → ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) )
106 105 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 𝐶 × 𝐼 ) ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) )
107 dffo3 ⊢ ( 𝐹 : 𝐵 –onto→ ( 𝐶 × 𝐼 ) ↔ ( 𝐹 : 𝐵 ⟶ ( 𝐶 × 𝐼 ) ∧ ∀ 𝑏 ∈ ( 𝐶 × 𝐼 ) ∃ 𝑎 ∈ 𝐵 𝑏 = ( 𝐹 ‘ 𝑎 ) ) )
108 13 106 107 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ ( 𝐶 × 𝐼 ) )