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

Metamath Proof Explorer

Theorem kmlem12

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004)

Ref Expression
Hypothesis kmlem9.1 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
Assertion kmlem12 ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kmlem9.1 ⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2 difeq1 ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
3 sneq ⊢ ( 𝑡 = 𝑧 → { 𝑡 } = { 𝑧 } )
4 3 difeq2d ⊢ ( 𝑡 = 𝑧 → ( 𝑥 ∖ { 𝑡 } ) = ( 𝑥 ∖ { 𝑧 } ) )
5 4 unieqd ⊢ ( 𝑡 = 𝑧 → ∪ ( 𝑥 ∖ { 𝑡 } ) = ∪ ( 𝑥 ∖ { 𝑧 } ) )
6 5 difeq2d ⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
7 2 6 eqtrd ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
8 7 neeq1d ⊢ ( 𝑡 = 𝑧 → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ ↔ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ) )
9 8 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ )
10 7 ineq1d ⊢ ( 𝑡 = 𝑧 → ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) = ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) )
11 10 eleq2d ⊢ ( 𝑡 = 𝑧 → ( 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ↔ 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) )
12 11 eubidv ⊢ ( 𝑡 = 𝑧 → ( ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) )
13 12 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) )
14 9 13 imbi12i ⊢ ( ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) )
15 in12 ⊢ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) = ( 𝑦 ∩ ( 𝑧 ∩ ∪ 𝐴 ) )
16 incom ⊢ ( 𝑦 ∩ ( 𝑧 ∩ ∪ 𝐴 ) ) = ( ( 𝑧 ∩ ∪ 𝐴 ) ∩ 𝑦 )
17 15 16 eqtri ⊢ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) = ( ( 𝑧 ∩ ∪ 𝐴 ) ∩ 𝑦 )
18 1 kmlem11 ⊢ ( 𝑧 ∈ 𝑥 → ( 𝑧 ∩ ∪ 𝐴 ) = ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
19 18 ineq1d ⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ∩ ∪ 𝐴 ) ∩ 𝑦 ) = ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) )
20 17 19 eqtr2id ⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) = ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) )
21 20 eleq2d ⊢ ( 𝑧 ∈ 𝑥 → ( 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
22 21 eubidv ⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
23 ax-1 ⊢ ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
24 22 23 biimtrdi ⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )
25 24 ralimia ⊢ ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) )
26 25 imim2i ⊢ ( ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑦 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )
27 14 26 sylbi ⊢ ( ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )
28 1 raleqi ⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
29 df-ral ⊢ ( ∀ 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
30 vex ⊢ 𝑧 ∈ V
31 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
32 31 rexbidv ⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ) )
33 30 32 elab ⊢ ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } ↔ ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) )
34 33 imbi1i ⊢ ( ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
35 r19.23v ⊢ ( ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∃ 𝑡 ∈ 𝑥 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
36 34 35 bitr4i ⊢ ( ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
37 36 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑧 ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
38 ralcom4 ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑧 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑧 ∀ 𝑡 ∈ 𝑥 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
39 vex ⊢ 𝑡 ∈ V
40 39 difexi ⊢ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∈ V
41 neeq1 ⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ ↔ ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ ) )
42 ineq1 ⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ∩ 𝑦 ) = ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) )
43 42 eleq2d ⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
44 43 eubidv ⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
45 41 44 imbi12d ⊢ ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) ) )
46 40 45 ceqsalv ⊢ ( ∀ 𝑧 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
47 46 ralbii ⊢ ( ∀ 𝑡 ∈ 𝑥 ∀ 𝑧 ( 𝑧 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
48 37 38 47 3bitr2i ⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) } → ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
49 28 29 48 3bitri ⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
50 ralim ⊢ ( ∀ 𝑡 ∈ 𝑥 ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) → ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
51 49 50 sylbi ⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ≠ ∅ → ∀ 𝑡 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) ∩ 𝑦 ) ) )
52 27 51 syl11 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑦 ∩ ∪ 𝐴 ) ) ) ) )