Metamath Proof Explorer

Theorem disjabrexf

Description: Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016) (Revised by Thierry Arnoux, 9-Mar-2017)

Ref Expression
Hypothesis disjabrexf.1 ⊢ Ⅎ 𝑥 𝐴
Assertion disjabrexf ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 )

Proof

Step Hyp Ref Expression
1 disjabrexf.1 ⊢ Ⅎ 𝑥 𝐴
2 nfdisj1 ⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝐵
3 nfcv ⊢ Ⅎ 𝑥 𝑦
4 1 nfcri ⊢ Ⅎ 𝑥 𝑖 ∈ 𝐴
5 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵
6 5 nfcri ⊢ Ⅎ 𝑥 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵
7 4 6 nfan ⊢ Ⅎ 𝑥 ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
8 7 nfab ⊢ Ⅎ 𝑥 { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) }
9 8 nfuni ⊢ Ⅎ 𝑥 ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) }
10 9 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵
11 10 nfeq1 ⊢ Ⅎ 𝑥 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦
12 3 11 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑗 ∈ 𝑦 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦
13 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦 ↔ ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝐵 ) )
14 13 raleqbi1dv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑗 ∈ 𝑦 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦 ↔ ∀ 𝑗 ∈ 𝐵 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝐵 ) )
15 vex ⊢ 𝑦 ∈ V
16 15 a1i ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ V )
17 simplll ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → Disj 𝑥 ∈ 𝐴 𝐵 )
18 simpllr ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
19 simprl ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → 𝑖 ∈ 𝐴 )
20 simplr ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → 𝑗 ∈ 𝐵 )
21 simprr ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
22 csbeq1a ⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
23 1 5 22 disjif2 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → 𝑥 = 𝑖 )
24 17 18 19 20 21 23 syl122anc ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ) → 𝑥 = 𝑖 )
25 simpr ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → 𝑥 = 𝑖 )
26 simpllr ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → 𝑥 ∈ 𝐴 )
27 25 26 eqeltrrd ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → 𝑖 ∈ 𝐴 )
28 simplr ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → 𝑗 ∈ 𝐵 )
29 22 eleq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) )
30 25 29 syl ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → ( 𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) )
31 28 30 mpbid ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
32 27 31 jca ⊢ ( ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) ∧ 𝑥 = 𝑖 ) → ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) )
33 24 32 impbida ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ↔ 𝑥 = 𝑖 ) )
34 equcom ⊢ ( 𝑥 = 𝑖 ↔ 𝑖 = 𝑥 )
35 33 34 bitrdi ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) ↔ 𝑖 = 𝑥 ) )
36 35 abbidv ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } = { 𝑖 ∣ 𝑖 = 𝑥 } )
37 df-sn ⊢ { 𝑥 } = { 𝑖 ∣ 𝑖 = 𝑥 }
38 36 37 eqtr4di ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } = { 𝑥 } )
39 38 unieqd ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } = ∪ { 𝑥 } )
40 vex ⊢ 𝑥 ∈ V
41 40 unisn ⊢ ∪ { 𝑥 } = 𝑥
42 39 41 eqtrdi ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } = 𝑥 )
43 csbeq1 ⊢ ( ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } = 𝑥 → ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = ⦋ 𝑥 / 𝑥 ⦌ 𝐵 )
44 csbid ⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐵 = 𝐵
45 43 44 eqtrdi ⊢ ( ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } = 𝑥 → ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝐵 )
46 42 45 syl ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐵 ) → ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝐵 )
47 46 ralrimiva ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑗 ∈ 𝐵 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝐵 )
48 2 12 14 16 47 elabreximd ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ∀ 𝑗 ∈ 𝑦 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦 )
49 48 ralrimiva ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ∀ 𝑗 ∈ 𝑦 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦 )
50 invdisj ⊢ ( ∀ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ∀ 𝑗 ∈ 𝑦 ⦋ ∪ { 𝑖 ∣ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) } / 𝑥 ⦌ 𝐵 = 𝑦 → Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 )
51 49 50 syl ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 )