bnj1408 - Mathbox for Jonathan Ben-Naim

	Mathbox for Jonathan Ben-Naim		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj1408		Structured version Visualization version GIF version

Theorem bnj1408 32312

Description: Technical lemma for bnj1414 32313. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
bnj1408.1	⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
bnj1408.2	⊢ 𝐶 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
bnj1408.3	⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
bnj1408.4	⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))

**Assertion**
Ref	Expression
bnj1408	⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Distinct variable groups: 𝑦,𝐴 𝑦,𝑅 𝑦,𝑋 Allowed substitution hints: 𝜃(𝑦) 𝜏(𝑦) 𝐵(𝑦) 𝐶(𝑦)

Proof of Theorem bnj1408 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj1408.3	. . . 4 ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
2	1	biimpri 230	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜃)
3		bnj1408.1	. . . . 5 ⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
4	3	bnj1413 32311	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
5		simplll 773	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
6		bnj213 32158	. . . . . . . . . . 11 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
7	6	sseli 3966	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → 𝑧 ∈ 𝐴)
8	7	adantl 484	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
9		bnj906 32206	. . . . . . . . 9 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
10	5, 8, 9	syl2anc 586	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
11		bnj1318 32301	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → trCl(𝑦, 𝐴, 𝑅) = trCl(𝑧, 𝐴, 𝑅))
12	11	ssiun2s 4975	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
13		ssun4 4154	. . . . . . . . . . 11 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
14	13, 3	sseqtrrdi 4021	. . . . . . . . . 10 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
15	12, 14	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
16	15	adantl 484	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
17	10, 16	sstrd 3980	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
18		simpr 487	. . . . . . . . . . 11 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
19	18	bnj1405 32112	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 ∈ pred (𝑋, 𝐴, 𝑅)𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
20		biid 263	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) ↔ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
21		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)
22		nfcv 2980	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 pred(𝑋, 𝐴, 𝑅)
23		nfiu1 4956	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
24	22, 23	nfun 4144	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
25	3, 24	nfcxfr 2978	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
26	25	nfcri 2974	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
27	21, 26	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵)
28	23	nfcri 2974	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
29	27, 28	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
30	29	nf5ri 2194	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∀𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
31	19, 20, 30	bnj1521 32127	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
32		simplll 773	. . . . . . . . . . . . 13 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
33	32	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
34		bnj1147 32270	. . . . . . . . . . . . 13 ⊢ trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
35		simp3 1134	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
36	34, 35	bnj1213 32074	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
37	33, 36, 9	syl2anc 586	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
38		simp2 1133	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ pred(𝑋, 𝐴, 𝑅))
39	6, 38	bnj1213 32074	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴)
40		bnj1125 32268	. . . . . . . . . . . 12 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
41	33, 39, 35, 40	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
42	37, 41	sstrd 3980	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
43		ssiun2 4974	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
44	43	3ad2ant2 1130	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
45		ssun4 4154	. . . . . . . . . . . 12 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
46	45, 3	sseqtrrdi 4021	. . . . . . . . . . 11 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
47	44, 46	syl 17	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
48	42, 47	sstrd 3980	. . . . . . . . 9 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
49	31, 48	bnj593 32020	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
50		nfcv 2980	. . . . . . . . . 10 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅)
51	50, 25	nfss 3963	. . . . . . . . 9 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵
52	51	nf5ri 2194	. . . . . . . 8 ⊢ ( pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵 → ∀𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
53	49, 52	bnj1397 32110	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
54		simpr 487	. . . . . . . 8 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
55	3	bnj1138 32064	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↔ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
56	54, 55	sylib 220	. . . . . . 7 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
57	17, 53, 56	mpjaodan 955	. . . . . 6 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
58	57	ralrimiva 3185	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
59		df-bnj19 31971	. . . . 5 ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
60	58, 59	sylibr 236	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅))
61	3	bnj931 32046	. . . . 5 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵
62	61	a1i 11	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
63		bnj1408.4	. . . 4 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
64	4, 60, 62, 63	syl3anbrc 1339	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜏)
65	1, 63	bnj1124 32264	. . 3 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
66	2, 64, 65	syl2anc 586	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
67		bnj906 32206	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
68		iunss1 4936	. . . . 5 ⊢ ( pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
69		unss2 4160	. . . . 5 ⊢ (∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
70	67, 68, 69	3syl 18	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
71		bnj1408.2	. . . 4 ⊢ 𝐶 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
72	70, 3, 71	3sstr4g 4015	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
73		biid 263	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
74		biid 263	. . . 4 ⊢ ((𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶) ↔ (𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶))
75	71, 73, 74	bnj1136 32273	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐶)
76	72, 75	sseqtrrd 4011	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ trCl(𝑋, 𝐴, 𝑅))
77	66, 76	eqssd 3987	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1536 ∈ wcel 2113 ∀wral 3141 Vcvv 3497 ∪ cun 3937 ⊆ wss 3939 ∪ ciun 4922 predc-bnj14 31962 FrSe w-bnj15 31966 trClc-bnj18 31968 TrFow-bnj19 31970

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-reg 9059 ax-inf2 9107

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-fal 1549 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-reu 3148 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-om 7584 df-1o 8105 df-bnj17 31961 df-bnj14 31963 df-bnj13 31965 df-bnj15 31967 df-bnj18 31969 df-bnj19 31971

This theorem is referenced by: bnj1414 32313

W3C validator