Description: Virtual deduction proof of onfrALTlem5 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem5 is onfrALTlem5VD without virtual deductions and was automatically derived from onfrALTlem5VD .
| 1:: | |- a e.V |
| 2:1: | |- ( a i^i x ) e. V |
| 3:2: | |- ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) ) |
| 4:3: | |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> -. ( a i^i x ) = (/) ) |
| 5:: | |- ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) ) |
| 6:4,5: | |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) ) |
| 7:2: | |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) ) |
| 8:: | |- ( b =/= (/) <-> -. b = (/) ) |
| 9:8: | |- A. b ( b =/= (/) <-> -. b = (/) ) |
| 10:2,9: | |- ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) ) |
| 11:7,10: | |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. b =/= (/) ) |
| 12:6,11: | |- ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) ) |
| 13:2: | |- ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) ) |
| 14:12,13: | |- ( ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ) |
| 15:2: | |- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) ) |
| 16:15,14: | |- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ) |
| 17:2: | |- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) |
| 18:2: | |- [_ ( a i^i x ) / b ]_ b = ( a i^i x ) |
| 19:2: | |- [_ ( a i^i x ) / b ]_ y = y |
| 20:18,19: | |- ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y ) |
| 21:17,20: | |- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y ) |
| 22:2: | |- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) ) |
| 23:2: | |- [_ ( a i^i x ) / b ]_ (/) = (/) |
| 24:21,23: | |- ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) ) |
| 25:22,24: | |- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) ) |
| 26:2: | |- ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) ) |
| 27:25,26: | |- ( ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) |
| 28:2: | |- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) ) |
| 29:27,28: | |- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) |
| 30:29: | |- A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) |
| 31:30: | |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) |
| 32:: | |- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) |
| 33:31,32: | |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) |
| 34:2: | |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) ) |
| 35:33,34: | |- ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) |
| 36:: | |- ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) ) |
| 37:36: | |- A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) ) |
| 38:2,37: | |- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) ) |
| 39:35,38: | |- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) |
| 40:16,39: | |- ( ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) ) |
| 41:2: | |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) ) |
| qed:40,41: | |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) ) |
| Ref | Expression | ||
|---|---|---|---|
| Assertion | onfrALTlem5VD | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | ⊢ 𝑎 ∈ V | |
| 2 | 1 | inex1 | ⊢ ( 𝑎 ∩ 𝑥 ) ∈ V |
| 3 | sbcimg | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) ) | |
| 4 | 2 3 | e0a | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) |
| 5 | sbcan | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ) ) | |
| 6 | sseq1 | ⊢ ( 𝑏 = ( 𝑎 ∩ 𝑥 ) → ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ↔ ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ) ) | |
| 7 | 2 6 | sbcie | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ↔ ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ) |
| 8 | df-ne | ⊢ ( 𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅ ) | |
| 9 | 8 | sbcbii | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ ) |
| 10 | sbcng | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ ↔ ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ) ) | |
| 11 | 10 | bicomd | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ ) ) |
| 12 | 2 11 | e0a | ⊢ ( ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ ) |
| 13 | eqsbc1 | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ ( 𝑎 ∩ 𝑥 ) = ∅ ) ) | |
| 14 | 2 13 | e0a | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ ( 𝑎 ∩ 𝑥 ) = ∅ ) |
| 15 | 14 | necon3bbii | ⊢ ( ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) |
| 16 | 9 12 15 | 3bitr2i | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ↔ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) |
| 17 | 7 16 | anbi12i | ⊢ ( ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ) ↔ ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) ) |
| 18 | 5 17 | bitri | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) ↔ ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) ) |
| 19 | df-rex | ⊢ ( ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ) | |
| 20 | 19 | sbcbii | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ) |
| 21 | sbcan | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ) ) | |
| 22 | sbcel2gv | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ) ) | |
| 23 | 2 22 | e0a | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ) |
| 24 | sbceqg | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ ) ) | |
| 25 | 2 24 | e0a | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ ) |
| 26 | csbin | ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ( ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 ∩ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 ) | |
| 27 | csbvarg | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 = ( 𝑎 ∩ 𝑥 ) ) | |
| 28 | 2 27 | e0a | ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 = ( 𝑎 ∩ 𝑥 ) |
| 29 | csbconstg | ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 = 𝑦 ) | |
| 30 | 2 29 | e0a | ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 = 𝑦 |
| 31 | 28 30 | ineq12i | ⊢ ( ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 ∩ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 ) = ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) |
| 32 | 26 31 | eqtri | ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) |
| 33 | csb0 | ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ = ∅ | |
| 34 | 32 33 | eqeq12i | ⊢ ( ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ ↔ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
| 35 | 25 34 | bitri | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
| 36 | 23 35 | anbi12i | ⊢ ( ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |
| 37 | 21 36 | bitri | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |
| 38 | 37 | exbii | ⊢ ( ∃ 𝑦 [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |
| 39 | sbcex2 | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑦 [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ) | |
| 40 | df-rex | ⊢ ( ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) | |
| 41 | 38 39 40 | 3bitr4i | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
| 42 | 20 41 | bitri | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
| 43 | 18 42 | imbi12i | ⊢ ( ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |
| 44 | 4 43 | bitri | ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) |