Theorem onfrALTlem2VD 45425

Description: Virtual deduction proof of onfrALTlem2 45083. 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. onfrALTlem2 45083 is onfrALTlem2VD 45425 without virtual deductions and was automatically derived from onfrALTlem2VD 45425.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   )
2:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑦)   )
3:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑎   )
4::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
5::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   )
6:5:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   )
7:4:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   )
8:6,7:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   )
9:8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   )
10:9:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Tr 𝑥   )
11:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
12:11:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ 𝑥   )
13:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑦   )
14:10,12,13:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑥   )
15:3,14:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑥)   )
16:13,15:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
17:16:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
18:17:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
19:18:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
20::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
21:20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
22:19,21:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑎 ∩ 𝑦) = ∅   )
23:20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
24:23:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   𝑦 ∈ 𝑎   )
25:22,24:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
26:25:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
27:26:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥 ) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
28:27:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥 ) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
29::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅   )
30:29:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
31:28,30:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
qed:31:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
onfrALTlem2VD	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Distinct variable groups:   𝑦,𝑎   𝑥,𝑦

Proof of Theorem onfrALTlem2VD

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn3 45152	. . . . . . . . . . . . . 14 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   )
2		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦)) → 𝑧 ∈ (𝑎 ∩ 𝑦))
3	1, 2	e3 45273	. . . . . . . . . . . . 13 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑦)   )
4		inss2 4187	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∩ 𝑦) ⊆ 𝑦
5	4	sseli 3930	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ 𝑦)
6	3, 5	e3 45273	. . . . . . . . . . . 12 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑦   )
7		inss1 4186	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∩ 𝑦) ⊆ 𝑎
8	7	sseli 3930	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ 𝑎)
9	3, 8	e3 45273	. . . . . . . . . . . . 13 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑎   )
10		idn2 45150	. . . . . . . . . . . . . . . . . 18 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   )
11		simpl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ 𝑎)
12	10, 11	e2 45168	. . . . . . . . . . . . . . . . 17 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   )
13		idn1 45111	. . . . . . . . . . . . . . . . . 18 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
14		simpl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ On)
15	13, 14	e1a 45164	. . . . . . . . . . . . . . . . 17 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   )
16		ssel 3928	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ On → (𝑥 ∈ 𝑎 → 𝑥 ∈ On))
17	16	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑎 → (𝑎 ⊆ On → 𝑥 ∈ On))
18	12, 15, 17	e21 45266	. . . . . . . . . . . . . . . 16 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   )
19		eloni 6351	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ On → Ord 𝑥)
20	18, 19	e2 45168	. . . . . . . . . . . . . . 15 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   )
21		ordtr 6355	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝑥 → Tr 𝑥)
22	20, 21	e2 45168	. . . . . . . . . . . . . 14 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Tr 𝑥   )
23		simpll 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦)) → 𝑦 ∈ (𝑎 ∩ 𝑥))
24	1, 23	e3 45273	. . . . . . . . . . . . . . 15 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
25		inss2 4187	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∩ 𝑥) ⊆ 𝑥
26	25	sseli 3930	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑎 ∩ 𝑥) → 𝑦 ∈ 𝑥)
27	24, 26	e3 45273	. . . . . . . . . . . . . 14 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ 𝑥   )
28		trel 5212	. . . . . . . . . . . . . . 15 ⊢ (Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
29	28	expcomd 420	. . . . . . . . . . . . . 14 ⊢ (Tr 𝑥 → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)))
30	22, 27, 6, 29	e233 45301	. . . . . . . . . . . . 13 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑥   )
31		elin 3918	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑎 ∩ 𝑥) ↔ (𝑧 ∈ 𝑎 ∧ 𝑧 ∈ 𝑥))
32	31	simplbi2 504	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑎 → (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝑎 ∩ 𝑥)))
33	9, 30, 32	e33 45270	. . . . . . . . . . . 12 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑥)   )
34		elin 3918	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦) ↔ (𝑧 ∈ (𝑎 ∩ 𝑥) ∧ 𝑧 ∈ 𝑦))
35	34	simplbi2com 506	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ (𝑎 ∩ 𝑥) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)))
36	6, 33, 35	e33 45270	. . . . . . . . . . 11 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
37	36	in3an 45148	. . . . . . . . . 10 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
38	37	gen31 45158	. . . . . . . . 9 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
39		df-ss 3919	. . . . . . . . . 10 ⊢ ((𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦) ↔ ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)))
40	39	biimpri 230	. . . . . . . . 9 ⊢ (∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)) → (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦))
41	38, 40	e3 45273	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
42		idn3 45152	. . . . . . . . 9 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
43		simpr 488	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
44	42, 43	e3 45273	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
45		sseq0 4354	. . . . . . . . 9 ⊢ (((𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑎 ∩ 𝑦) = ∅)
46	45	ex 416	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦) → (((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ → (𝑎 ∩ 𝑦) = ∅))
47	41, 44, 46	e33 45270	. . . . . . 7 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑎 ∩ 𝑦) = ∅   )
48		simpl 486	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → 𝑦 ∈ (𝑎 ∩ 𝑥))
49	42, 48	e3 45273	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
50		inss1 4186	. . . . . . . . 9 ⊢ (𝑎 ∩ 𝑥) ⊆ 𝑎
51	50	sseli 3930	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑎 ∩ 𝑥) → 𝑦 ∈ 𝑎)
52	49, 51	e3 45273	. . . . . . 7 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   𝑦 ∈ 𝑎   )
53		pm3.21 475	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑦) = ∅ → (𝑦 ∈ 𝑎 → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
54	47, 52, 53	e33 45270	. . . . . 6 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
55	54	in3 45146	. . . . 5 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
56	55	gen21 45156	. . . 4 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
57		exim 1853	. . . 4 ⊢ (∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) → (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
58	56, 57	e2 45168	. . 3 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
59		onfrALTlem3VD 45423	. . . 4 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
60		df-rex 3086	. . . . 5 ⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
61	60	biimpi 218	. . . 4 ⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ → ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
62	59, 61	e2 45168	. . 3 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
63		id 22	. . 3 ⊢ ((∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) → (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
64	58, 62, 63	e22 45208	. 2 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
65		df-rex 3086	. . 3 ⊢ (∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
66	65	biimpri 230	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)
67	64, 66	e2 45168	1 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ≠ wne 2956  ∃wrex 3085   ∩ cin 3901   ⊆ wss 3902  ∅c0 4283  Tr wtr 5204  Ord word 6340  Oncon0 6341  (   wvd2 45114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-tr 5205  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-ord 6344  df-on 6345  df-vd1 45107  df-vd2 45115  df-vd3 45127

This theorem is referenced by:  onfrALTVD  45427