ldgenpisyslem1

	Ref	Expression
Hypotheses	dynkin.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
	dynkin.l	$⊢ L = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s))\}$
	dynkin.o	$⊢ φ \to O \in V$
	ldgenpisys.e	$⊢ E = ⋂ \{t \in L \| T \subseteq t\}$
	ldgenpisys.1	$⊢ φ \to T \in P$
	ldgenpisyslem1.1	$⊢ φ \to A \in E$
Assertion	ldgenpisyslem1	$⊢ φ \to \{b \in 𝒫 O \| A \cap b \in E\} \in L$

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
2		dynkin.l	$⊢ L = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s))\}$
3		dynkin.o	$⊢ φ \to O \in V$
4		ldgenpisys.e	$⊢ E = ⋂ \{t \in L \| T \subseteq t\}$
5		ldgenpisys.1	$⊢ φ \to T \in P$
6		ldgenpisyslem1.1	$⊢ φ \to A \in E$
7		ssrab2	$⊢ \{b \in 𝒫 O \| A \cap b \in E\} \subseteq 𝒫 O$
8		pwexg	$⊢ O \in V \to 𝒫 O \in V$
9		rabexg	$⊢ 𝒫 O \in V \to \{b \in 𝒫 O \| A \cap b \in E\} \in V$
10		elpwg	$⊢ \{b \in 𝒫 O \| A \cap b \in E\} \in V \to (\{b \in 𝒫 O \| A \cap b \in E\} \in 𝒫 𝒫 O \leftrightarrow \{b \in 𝒫 O \| A \cap b \in E\} \subseteq 𝒫 O)$
11	3 8 9 10	4syl	$⊢ φ \to (\{b \in 𝒫 O \| A \cap b \in E\} \in 𝒫 𝒫 O \leftrightarrow \{b \in 𝒫 O \| A \cap b \in E\} \subseteq 𝒫 O)$
12	7 11	mpbiri	$⊢ φ \to \{b \in 𝒫 O \| A \cap b \in E\} \in 𝒫 𝒫 O$
13		ineq2	$⊢ b = \emptyset \to A \cap b = A \cap \emptyset$
14	13	eleq1d	$⊢ b = \emptyset \to (A \cap b \in E \leftrightarrow A \cap \emptyset \in E)$
15		0elpw	$⊢ \emptyset \in 𝒫 O$
16	15	a1i	$⊢ φ \to \emptyset \in 𝒫 O$
17	2	isldsys	$⊢ t \in L \leftrightarrow (t \in 𝒫 𝒫 O \land (\emptyset \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)))$
18	17	simprbi	$⊢ t \in L \to (\emptyset \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t))$
19	18	simp1d	$⊢ t \in L \to \emptyset \in t$
20	19	ad2antlr	$⊢ ((φ \land t \in L) \land T \subseteq t) \to \emptyset \in t$
21	20	ex	$⊢ (φ \land t \in L) \to (T \subseteq t \to \emptyset \in t)$
22	21	ralrimiva	$⊢ φ \to \forall t \in L (T \subseteq t \to \emptyset \in t)$
23		0ex	$⊢ \emptyset \in V$
24	23	elintrab	$⊢ \emptyset \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to \emptyset \in t)$
25	22 24	sylibr	$⊢ φ \to \emptyset \in ⋂ \{t \in L \| T \subseteq t\}$
26		in0	$⊢ A \cap \emptyset = \emptyset$
27	25 26 4	3eltr4g	$⊢ φ \to A \cap \emptyset \in E$
28	14 16 27	elrabd	$⊢ φ \to \emptyset \in \{b \in 𝒫 O \| A \cap b \in E\}$
29		ineq2	$⊢ b = x \to A \cap b = A \cap x$
30	29	eleq1d	$⊢ b = x \to (A \cap b \in E \leftrightarrow A \cap x \in E)$
31	30	elrab	$⊢ x \in \{b \in 𝒫 O \| A \cap b \in E\} \leftrightarrow (x \in 𝒫 O \land A \cap x \in E)$
32		pwidg	$⊢ O \in V \to O \in 𝒫 O$
33	3 32	syl	$⊢ φ \to O \in 𝒫 O$
34	33	adantr	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to O \in 𝒫 O$
35	34	elpwdifcl	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to O ∖ x \in 𝒫 O$
36	2	pwldsys	$⊢ O \in V \to 𝒫 O \in L$
37	3 36	syl	$⊢ φ \to 𝒫 O \in L$
38	1	ispisys	$⊢ T \in P \leftrightarrow (T \in 𝒫 𝒫 O \land fi (T) \subseteq T)$
39	5 38	sylib	$⊢ φ \to (T \in 𝒫 𝒫 O \land fi (T) \subseteq T)$
40	39	simpld	$⊢ φ \to T \in 𝒫 𝒫 O$
41	40	elpwid	$⊢ φ \to T \subseteq 𝒫 O$
42		sseq2	$⊢ t = 𝒫 O \to (T \subseteq t \leftrightarrow T \subseteq 𝒫 O)$
43	42	intminss	$⊢ (𝒫 O \in L \land T \subseteq 𝒫 O) \to ⋂ \{t \in L \| T \subseteq t\} \subseteq 𝒫 O$
44	37 41 43	syl2anc	$⊢ φ \to ⋂ \{t \in L \| T \subseteq t\} \subseteq 𝒫 O$
45	4 44	eqsstrid	$⊢ φ \to E \subseteq 𝒫 O$
46	45 6	sseldd	$⊢ φ \to A \in 𝒫 O$
47	46	elpwid	$⊢ φ \to A \subseteq O$
48	47	ad3antrrr	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \subseteq O$
49		difin	$⊢ A ∖ (A \cap x) = A ∖ x$
50		difin2	$⊢ A \subseteq O \to A ∖ x = (O ∖ x) \cap A$
51	49 50	syl5eq	$⊢ A \subseteq O \to A ∖ (A \cap x) = (O ∖ x) \cap A$
52		incom	$⊢ (O ∖ x) \cap A = A \cap (O ∖ x)$
53	51 52	eqtrdi	$⊢ A \subseteq O \to A ∖ (A \cap x) = A \cap (O ∖ x)$
54		difuncomp	$⊢ A \subseteq O \to A ∖ (A \cap x) = O ∖ ((O ∖ A) \cup (A \cap x))$
55	53 54	eqtr3d	$⊢ A \subseteq O \to A \cap (O ∖ x) = O ∖ ((O ∖ A) \cup (A \cap x))$
56	48 55	syl	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \cap (O ∖ x) = O ∖ ((O ∖ A) \cup (A \cap x))$
57		difeq2	$⊢ y = (O ∖ A) \cup (A \cap x) \to O ∖ y = O ∖ ((O ∖ A) \cup (A \cap x))$
58	57	eleq1d	$⊢ y = (O ∖ A) \cup (A \cap x) \to (O ∖ y \in t \leftrightarrow O ∖ ((O ∖ A) \cup (A \cap x)) \in t)$
59	18	simp2d	$⊢ t \in L \to \forall x \in t O ∖ x \in t$
60	59	ad2antlr	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to \forall x \in t O ∖ x \in t$
61		difeq2	$⊢ x = y \to O ∖ x = O ∖ y$
62	61	eleq1d	$⊢ x = y \to (O ∖ x \in t \leftrightarrow O ∖ y \in t)$
63	62	cbvralvw	$⊢ \forall x \in t O ∖ x \in t \leftrightarrow \forall y \in t O ∖ y \in t$
64	60 63	sylib	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to \forall y \in t O ∖ y \in t$
65		simplr	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to t \in L$
66	6 4	eleqtrdi	$⊢ φ \to A \in ⋂ \{t \in L \| T \subseteq t\}$
67		elintrabg	$⊢ A \in E \to (A \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \in t))$
68	6 67	syl	$⊢ φ \to (A \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \in t))$
69	66 68	mpbid	$⊢ φ \to \forall t \in L (T \subseteq t \to A \in t)$
70	69	r19.21bi	$⊢ (φ \land t \in L) \to (T \subseteq t \to A \in t)$
71	70	imp	$⊢ ((φ \land t \in L) \land T \subseteq t) \to A \in t$
72	71	adantllr	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \in t$
73		difeq2	$⊢ x = A \to O ∖ x = O ∖ A$
74	73	eleq1d	$⊢ x = A \to (O ∖ x \in t \leftrightarrow O ∖ A \in t)$
75	59	adantr	$⊢ (t \in L \land A \in t) \to \forall x \in t O ∖ x \in t$
76		simpr	$⊢ (t \in L \land A \in t) \to A \in t$
77	74 75 76	rspcdva	$⊢ (t \in L \land A \in t) \to O ∖ A \in t$
78	65 72 77	syl2anc	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to O ∖ A \in t$
79		simpllr	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to (x \in 𝒫 O \land A \cap x \in E)$
80	79	simprd	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \cap x \in E$
81	80 4	eleqtrdi	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \cap x \in ⋂ \{t \in L \| T \subseteq t\}$
82		vex	$⊢ x \in V$
83	82	inex2	$⊢ A \cap x \in V$
84		elintrabg	$⊢ A \cap x \in V \to (A \cap x \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \cap x \in t))$
85	83 84	mp1i	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to (A \cap x \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \cap x \in t))$
86	81 85	mpbid	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to \forall t \in L (T \subseteq t \to A \cap x \in t)$
87		simpr	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to T \subseteq t$
88		rspa	$⊢ (\forall t \in L (T \subseteq t \to A \cap x \in t) \land t \in L) \to (T \subseteq t \to A \cap x \in t)$
89	88	imp	$⊢ ((\forall t \in L (T \subseteq t \to A \cap x \in t) \land t \in L) \land T \subseteq t) \to A \cap x \in t$
90	86 65 87 89	syl21anc	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \cap x \in t$
91		incom	$⊢ (O ∖ A) \cap (A \cap x) = (A \cap x) \cap (O ∖ A)$
92		inss1	$⊢ A \cap x \subseteq A$
93		disjdif	$⊢ A \cap (O ∖ A) = \emptyset$
94		ssdisj	$⊢ (A \cap x \subseteq A \land A \cap (O ∖ A) = \emptyset) \to (A \cap x) \cap (O ∖ A) = \emptyset$
95	92 93 94	mp2an	$⊢ (A \cap x) \cap (O ∖ A) = \emptyset$
96	91 95	eqtri	$⊢ (O ∖ A) \cap (A \cap x) = \emptyset$
97	96	a1i	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to (O ∖ A) \cap (A \cap x) = \emptyset$
98	2 65 78 90 97	unelldsys	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to (O ∖ A) \cup (A \cap x) \in t$
99	58 64 98	rspcdva	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to O ∖ ((O ∖ A) \cup (A \cap x)) \in t$
100	56 99	eqeltrd	$⊢ (((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \land T \subseteq t) \to A \cap (O ∖ x) \in t$
101	100	ex	$⊢ ((φ \land (x \in 𝒫 O \land A \cap x \in E)) \land t \in L) \to (T \subseteq t \to A \cap (O ∖ x) \in t)$
102	101	ralrimiva	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to \forall t \in L (T \subseteq t \to A \cap (O ∖ x) \in t)$
103		inex1g	$⊢ A \in E \to A \cap (O ∖ x) \in V$
104	6 103	syl	$⊢ φ \to A \cap (O ∖ x) \in V$
105	104	adantr	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to A \cap (O ∖ x) \in V$
106		elintrabg	$⊢ A \cap (O ∖ x) \in V \to (A \cap (O ∖ x) \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \cap (O ∖ x) \in t))$
107	105 106	syl	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to (A \cap (O ∖ x) \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \cap (O ∖ x) \in t))$
108	102 107	mpbird	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to A \cap (O ∖ x) \in ⋂ \{t \in L \| T \subseteq t\}$
109	108 4	eleqtrrdi	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to A \cap (O ∖ x) \in E$
110	35 109	jca	$⊢ (φ \land (x \in 𝒫 O \land A \cap x \in E)) \to (O ∖ x \in 𝒫 O \land A \cap (O ∖ x) \in E)$
111	31 110	sylan2b	$⊢ (φ \land x \in \{b \in 𝒫 O \| A \cap b \in E\}) \to (O ∖ x \in 𝒫 O \land A \cap (O ∖ x) \in E)$
112		ineq2	$⊢ b = O ∖ x \to A \cap b = A \cap (O ∖ x)$
113	112	eleq1d	$⊢ b = O ∖ x \to (A \cap b \in E \leftrightarrow A \cap (O ∖ x) \in E)$
114	113	elrab	$⊢ O ∖ x \in \{b \in 𝒫 O \| A \cap b \in E\} \leftrightarrow (O ∖ x \in 𝒫 O \land A \cap (O ∖ x) \in E)$
115	111 114	sylibr	$⊢ (φ \land x \in \{b \in 𝒫 O \| A \cap b \in E\}) \to O ∖ x \in \{b \in 𝒫 O \| A \cap b \in E\}$
116	115	ralrimiva	$⊢ φ \to \forall x \in \{b \in 𝒫 O \| A \cap b \in E\} O ∖ x \in \{b \in 𝒫 O \| A \cap b \in E\}$
117		ineq2	$⊢ b = ⋃ x \to A \cap b = A \cap ⋃ x$
118	117	eleq1d	$⊢ b = ⋃ x \to (A \cap b \in E \leftrightarrow A \cap ⋃ x \in E)$
119	7	sspwi	$⊢ 𝒫 \{b \in 𝒫 O \| A \cap b \in E\} \subseteq 𝒫 𝒫 O$
120		simplr	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}$
121	119 120	sseldi	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x \in 𝒫 𝒫 O$
122	121	elpwunicl	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ⋃ x \in 𝒫 O$
123		uniin2	$⊢ ⋃_{y \in x} (A \cap y) = A \cap ⋃ x$
124		vex	$⊢ y \in V$
125	124	inex2	$⊢ A \cap y \in V$
126	125	dfiun3	$⊢ ⋃_{y \in x} (A \cap y) = ⋃ ran (y \in x ⟼ A \cap y)$
127	123 126	eqtr3i	$⊢ A \cap ⋃ x = ⋃ ran (y \in x ⟼ A \cap y)$
128		simplr	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to t \in L$
129		nfv	$⊢ Ⅎ y (φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\})$
130		nfv	$⊢ Ⅎ y x ≼ ω$
131		nfdisj1	$⊢ Ⅎ y \underset{y \in x}{Disj} y$
132	130 131	nfan	$⊢ Ⅎ y (x ≼ ω \land \underset{y \in x}{Disj} y)$
133	129 132	nfan	$⊢ Ⅎ y ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y))$
134		nfv	$⊢ Ⅎ y t \in L$
135	133 134	nfan	$⊢ Ⅎ y (((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L)$
136		nfv	$⊢ Ⅎ y T \subseteq t$
137	135 136	nfan	$⊢ Ⅎ y ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t)$
138		elpwi	$⊢ x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\} \to x \subseteq \{b \in 𝒫 O \| A \cap b \in E\}$
139	138	ad4antlr	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to x \subseteq \{b \in 𝒫 O \| A \cap b \in E\}$
140	139	sselda	$⊢ (((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \land y \in x) \to y \in \{b \in 𝒫 O \| A \cap b \in E\}$
141		ineq2	$⊢ b = y \to A \cap b = A \cap y$
142	141	eleq1d	$⊢ b = y \to (A \cap b \in E \leftrightarrow A \cap y \in E)$
143	142	elrab	$⊢ y \in \{b \in 𝒫 O \| A \cap b \in E\} \leftrightarrow (y \in 𝒫 O \land A \cap y \in E)$
144	143	simprbi	$⊢ y \in \{b \in 𝒫 O \| A \cap b \in E\} \to A \cap y \in E$
145	140 144	syl	$⊢ (((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \land y \in x) \to A \cap y \in E$
146		simpllr	$⊢ (((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \land y \in x) \to t \in L$
147		simplr	$⊢ (((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \land y \in x) \to T \subseteq t$
148	4	eleq2i	$⊢ A \cap y \in E \leftrightarrow A \cap y \in ⋂ \{t \in L \| T \subseteq t\}$
149	125	elintrab	$⊢ A \cap y \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \cap y \in t)$
150	148 149	bitri	$⊢ A \cap y \in E \leftrightarrow \forall t \in L (T \subseteq t \to A \cap y \in t)$
151		rspa	$⊢ (\forall t \in L (T \subseteq t \to A \cap y \in t) \land t \in L) \to (T \subseteq t \to A \cap y \in t)$
152	150 151	sylanb	$⊢ (A \cap y \in E \land t \in L) \to (T \subseteq t \to A \cap y \in t)$
153	152	imp	$⊢ ((A \cap y \in E \land t \in L) \land T \subseteq t) \to A \cap y \in t$
154	145 146 147 153	syl21anc	$⊢ (((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \land y \in x) \to A \cap y \in t$
155	154	ex	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to (y \in x \to A \cap y \in t)$
156	137 155	ralrimi	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to \forall y \in x A \cap y \in t$
157		eqid	$⊢ (y \in x ⟼ A \cap y) = (y \in x ⟼ A \cap y)$
158	157	rnmptss	$⊢ \forall y \in x A \cap y \in t \to ran (y \in x ⟼ A \cap y) \subseteq t$
159	156 158	syl	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to ran (y \in x ⟼ A \cap y) \subseteq t$
160	128 159	sselpwd	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to ran (y \in x ⟼ A \cap y) \in 𝒫 t$
161		simpllr	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to (x ≼ ω \land \underset{y \in x}{Disj} y)$
162	161	simpld	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to x ≼ ω$
163		1stcrestlem	$⊢ x ≼ ω \to ran (y \in x ⟼ A \cap y) ≼ ω$
164	162 163	syl	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to ran (y \in x ⟼ A \cap y) ≼ ω$
165	161	simprd	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to \underset{y \in x}{Disj} y$
166		disjin2	$⊢ \underset{y \in x}{Disj} y \to \underset{y \in x}{Disj} (A \cap y)$
167		disjrnmpt	$⊢ \underset{y \in x}{Disj} (A \cap y) \to \underset{z \in ran (y \in x ⟼ A \cap y)}{Disj} z$
168	165 166 167	3syl	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to \underset{z \in ran (y \in x ⟼ A \cap y)}{Disj} z$
169		nfmpt1	$⊢ \underline{Ⅎ} y (y \in x ⟼ A \cap y)$
170	169	nfrn	$⊢ \underline{Ⅎ} y ran (y \in x ⟼ A \cap y)$
171		nfcv	$⊢ \underline{Ⅎ} z y$
172		nfcv	$⊢ \underline{Ⅎ} y z$
173		id	$⊢ y = z \to y = z$
174	170 171 172 173	cbvdisjf	$⊢ \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y \leftrightarrow \underset{z \in ran (y \in x ⟼ A \cap y)}{Disj} z$
175	168 174	sylibr	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y$
176		breq1	$⊢ z = ran (y \in x ⟼ A \cap y) \to (z ≼ ω \leftrightarrow ran (y \in x ⟼ A \cap y) ≼ ω)$
177	172 170	disjeq1f	$⊢ z = ran (y \in x ⟼ A \cap y) \to (\underset{y \in z}{Disj} y \leftrightarrow \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y)$
178	176 177	anbi12d	$⊢ z = ran (y \in x ⟼ A \cap y) \to ((z ≼ ω \land \underset{y \in z}{Disj} y) \leftrightarrow (ran (y \in x ⟼ A \cap y) ≼ ω \land \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y))$
179		unieq	$⊢ z = ran (y \in x ⟼ A \cap y) \to ⋃ z = ⋃ ran (y \in x ⟼ A \cap y)$
180	179	eleq1d	$⊢ z = ran (y \in x ⟼ A \cap y) \to (⋃ z \in t \leftrightarrow ⋃ ran (y \in x ⟼ A \cap y) \in t)$
181	178 180	imbi12d	$⊢ z = ran (y \in x ⟼ A \cap y) \to (((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in t) \leftrightarrow ((ran (y \in x ⟼ A \cap y) ≼ ω \land \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y) \to ⋃ ran (y \in x ⟼ A \cap y) \in t))$
182	18	simp3d	$⊢ t \in L \to \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)$
183		breq1	$⊢ x = z \to (x ≼ ω \leftrightarrow z ≼ ω)$
184		disjeq1	$⊢ x = z \to (\underset{y \in x}{Disj} y \leftrightarrow \underset{y \in z}{Disj} y)$
185	183 184	anbi12d	$⊢ x = z \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \leftrightarrow (z ≼ ω \land \underset{y \in z}{Disj} y))$
186		unieq	$⊢ x = z \to ⋃ x = ⋃ z$
187	186	eleq1d	$⊢ x = z \to (⋃ x \in t \leftrightarrow ⋃ z \in t)$
188	185 187	imbi12d	$⊢ x = z \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t) \leftrightarrow ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in t))$
189	188	cbvralvw	$⊢ \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t) \leftrightarrow \forall z \in 𝒫 t ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in t)$
190	182 189	sylib	$⊢ t \in L \to \forall z \in 𝒫 t ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in t)$
191	190	adantr	$⊢ (t \in L \land ran (y \in x ⟼ A \cap y) \in 𝒫 t) \to \forall z \in 𝒫 t ((z ≼ ω \land \underset{y \in z}{Disj} y) \to ⋃ z \in t)$
192		simpr	$⊢ (t \in L \land ran (y \in x ⟼ A \cap y) \in 𝒫 t) \to ran (y \in x ⟼ A \cap y) \in 𝒫 t$
193	181 191 192	rspcdva	$⊢ (t \in L \land ran (y \in x ⟼ A \cap y) \in 𝒫 t) \to ((ran (y \in x ⟼ A \cap y) ≼ ω \land \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y) \to ⋃ ran (y \in x ⟼ A \cap y) \in t)$
194	193	imp	$⊢ ((t \in L \land ran (y \in x ⟼ A \cap y) \in 𝒫 t) \land (ran (y \in x ⟼ A \cap y) ≼ ω \land \underset{y \in ran (y \in x ⟼ A \cap y)}{Disj} y)) \to ⋃ ran (y \in x ⟼ A \cap y) \in t$
195	128 160 164 175 194	syl22anc	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to ⋃ ran (y \in x ⟼ A \cap y) \in t$
196	127 195	eqeltrid	$⊢ ((((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \land T \subseteq t) \to A \cap ⋃ x \in t$
197	196	ex	$⊢ (((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \land t \in L) \to (T \subseteq t \to A \cap ⋃ x \in t)$
198	197	ralrimiva	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to \forall t \in L (T \subseteq t \to A \cap ⋃ x \in t)$
199		vuniex	$⊢ ⋃ x \in V$
200	199	inex2	$⊢ A \cap ⋃ x \in V$
201	200	elintrab	$⊢ A \cap ⋃ x \in ⋂ \{t \in L \| T \subseteq t\} \leftrightarrow \forall t \in L (T \subseteq t \to A \cap ⋃ x \in t)$
202	198 201	sylibr	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to A \cap ⋃ x \in ⋂ \{t \in L \| T \subseteq t\}$
203	202 4	eleqtrrdi	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to A \cap ⋃ x \in E$
204	118 122 203	elrabd	$⊢ ((φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ⋃ x \in \{b \in 𝒫 O \| A \cap b \in E\}$
205	204	ex	$⊢ (φ \land x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\}) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in \{b \in 𝒫 O \| A \cap b \in E\})$
206	205	ralrimiva	$⊢ φ \to \forall x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\} ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in \{b \in 𝒫 O \| A \cap b \in E\})$
207	28 116 206	3jca	$⊢ φ \to (\emptyset \in \{b \in 𝒫 O \| A \cap b \in E\} \land \forall x \in \{b \in 𝒫 O \| A \cap b \in E\} O ∖ x \in \{b \in 𝒫 O \| A \cap b \in E\} \land \forall x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\} ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in \{b \in 𝒫 O \| A \cap b \in E\}))$
208	2	isldsys	$⊢ \{b \in 𝒫 O \| A \cap b \in E\} \in L \leftrightarrow (\{b \in 𝒫 O \| A \cap b \in E\} \in 𝒫 𝒫 O \land (\emptyset \in \{b \in 𝒫 O \| A \cap b \in E\} \land \forall x \in \{b \in 𝒫 O \| A \cap b \in E\} O ∖ x \in \{b \in 𝒫 O \| A \cap b \in E\} \land \forall x \in 𝒫 \{b \in 𝒫 O \| A \cap b \in E\} ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in \{b \in 𝒫 O \| A \cap b \in E\})))$
209	12 207 208	sylanbrc	$⊢ φ \to \{b \in 𝒫 O \| A \cap b \in E\} \in L$

Metamath Proof Explorer

Theorem ldgenpisyslem1

Proof