Metamath Proof Explorer

Theorem disjabrex

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

Ref Expression
Assertion disjabrex ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 )

Proof

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