This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1iun

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013) (Revised by Mario Carneiro, 24-Jun-2015) (Proof shortened by AV, 5-Nov-2023)

Ref Expression
Hypotheses fiun.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
fiun.2 ⊢ 𝐵 ∈ V
Assertion f1iun ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 –1-1→ 𝑆 )

Proof

Step Hyp Ref Expression
1 fiun.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2 fiun.2 ⊢ 𝐵 ∈ V
3 vex ⊢ 𝑢 ∈ V
4 eqeq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 = 𝐵 ↔ 𝑢 = 𝐵 ) )
5 4 rexbidv ⊢ ( 𝑧 = 𝑢 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) )
6 3 5 elab ⊢ ( 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 )
7 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) )
8 nfv ⊢ Ⅎ 𝑥 ( Fun 𝑢 ∧ Fun ◡ 𝑢 )
9 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵
10 9 nfab ⊢ Ⅎ 𝑥 { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
11 nfv ⊢ Ⅎ 𝑥 ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 )
12 10 11 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 )
13 8 12 nfan ⊢ Ⅎ 𝑥 ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
14 f1eq1 ⊢ ( 𝑢 = 𝐵 → ( 𝑢 : 𝐷 –1-1→ 𝑆 ↔ 𝐵 : 𝐷 –1-1→ 𝑆 ) )
15 14 biimparc ⊢ ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ 𝑢 = 𝐵 ) → 𝑢 : 𝐷 –1-1→ 𝑆 )
16 df-f1 ⊢ ( 𝑢 : 𝐷 –1-1→ 𝑆 ↔ ( 𝑢 : 𝐷 ⟶ 𝑆 ∧ Fun ◡ 𝑢 ) )
17 ffun ⊢ ( 𝑢 : 𝐷 ⟶ 𝑆 → Fun 𝑢 )
18 17 anim1i ⊢ ( ( 𝑢 : 𝐷 ⟶ 𝑆 ∧ Fun ◡ 𝑢 ) → ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) )
19 16 18 sylbi ⊢ ( 𝑢 : 𝐷 –1-1→ 𝑆 → ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) )
20 15 19 syl ⊢ ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) )
21 20 adantlr ⊢ ( ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) )
22 f1f ⊢ ( 𝐵 : 𝐷 –1-1→ 𝑆 → 𝐵 : 𝐷 ⟶ 𝑆 )
23 1 fiunlem ⊢ ( ( ( 𝐵 : 𝐷 ⟶ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
24 22 23 sylanl1 ⊢ ( ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) )
25 21 24 jca ⊢ ( ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
26 25 a1i ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
27 13 26 rexlimi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 = 𝐵 ) → ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
28 7 27 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑢 = 𝐵 ) → ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
29 6 28 sylan2b ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) ∧ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) → ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
30 29 ralrimiva ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∀ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
31 fun11uni ⊢ ( ∀ 𝑢 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( ( Fun 𝑢 ∧ Fun ◡ 𝑢 ) ∧ ∀ 𝑣 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) → ( Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ∧ Fun ◡ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) )
32 30 31 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ∧ Fun ◡ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } ) )
33 32 simpld ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
34 2 dfiun2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
35 34 funeqi ⊢ ( Fun ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
36 33 35 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ∪ 𝑥 ∈ 𝐴 𝐵 )
37 3 eldm2 ⊢ ( 𝑢 ∈ dom 𝐵 ↔ ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
38 f1dm ⊢ ( 𝐵 : 𝐷 –1-1→ 𝑆 → dom 𝐵 = 𝐷 )
39 38 eleq2d ⊢ ( 𝐵 : 𝐷 –1-1→ 𝑆 → ( 𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
40 37 39 bitr3id ⊢ ( 𝐵 : 𝐷 –1-1→ 𝑆 → ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
41 40 adantr ⊢ ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷 ) )
42 41 ralrexbid ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ 𝐷 ) )
43 eliun ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
44 43 exbii ⊢ ( ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
45 3 eldm2 ⊢ ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
46 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ↔ ∃ 𝑣 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
47 44 45 46 3bitr4i ⊢ ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
48 eliun ⊢ ( 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 ∈ 𝐷 )
49 42 47 48 3bitr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ( 𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ) )
50 49 eqrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷 )
51 df-fn ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ( Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷 ) )
52 36 50 51 sylanbrc ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 )
53 rniun ⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵
54 22 frnd ⊢ ( 𝐵 : 𝐷 –1-1→ 𝑆 → ran 𝐵 ⊆ 𝑆 )
55 54 adantr ⊢ ( ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ran 𝐵 ⊆ 𝑆 )
56 55 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
57 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
58 56 57 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 )
59 53 58 eqsstrid ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆 )
60 df-f ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪ 𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆 ) )
61 52 59 60 sylanbrc ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 )
62 32 simprd ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ◡ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
63 34 cnveqi ⊢ ◡ ∪ 𝑥 ∈ 𝐴 𝐵 = ◡ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 }
64 63 funeqi ⊢ ( Fun ◡ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } )
65 62 64 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → Fun ◡ ∪ 𝑥 ∈ 𝐴 𝐵 )
66 df-f1 ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 –1-1→ 𝑆 ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 ⟶ 𝑆 ∧ Fun ◡ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
67 61 65 66 sylanbrc ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 : 𝐷 –1-1→ 𝑆 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 : ∪ 𝑥 ∈ 𝐴 𝐷 –1-1→ 𝑆 )