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 32418

Description: Technical lemma for bnj1414 32419. 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 231	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜃)
3		bnj1408.1	. . . . 5 ⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
4	3	bnj1413 32417	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
5		simplll 774	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
6		bnj213 32264	. . . . . . . . . . 11 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
7	6	sseli 3911	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → 𝑧 ∈ 𝐴)
8	7	adantl 485	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
9		bnj906 32312	. . . . . . . . 9 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
10	5, 8, 9	syl2anc 587	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
11		bnj1318 32407	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → trCl(𝑦, 𝐴, 𝑅) = trCl(𝑧, 𝐴, 𝑅))
12	11	ssiun2s 4935	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
13		ssun4 4102	. . . . . . . . . . 11 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
14	13, 3	sseqtrrdi 3966	. . . . . . . . . 10 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
15	12, 14	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
16	15	adantl 485	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
17	10, 16	sstrd 3925	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
18		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
19	18	bnj1405 32218	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 ∈ pred (𝑋, 𝐴, 𝑅)𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
20		biid 264	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) ↔ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
21		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)
22		nfcv 2955	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 pred(𝑋, 𝐴, 𝑅)
23		nfiu1 4915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
24	22, 23	nfun 4092	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
25	3, 24	nfcxfr 2953	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
26	25	nfcri 2943	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
27	21, 26	nfan 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵)
28	23	nfcri 2943	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
29	27, 28	nfan 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
30	29	nf5ri 2193	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∀𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
31	19, 20, 30	bnj1521 32233	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
32		simplll 774	. . . . . . . . . . . . 13 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
33	32	3ad2ant1 1130	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
34		bnj1147 32376	. . . . . . . . . . . . 13 ⊢ trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
35		simp3 1135	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
36	34, 35	bnj1213 32180	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
37	33, 36, 9	syl2anc 587	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
38		simp2 1134	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ pred(𝑋, 𝐴, 𝑅))
39	6, 38	bnj1213 32180	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴)
40		bnj1125 32374	. . . . . . . . . . . 12 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
41	33, 39, 35, 40	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
42	37, 41	sstrd 3925	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
43		ssiun2 4934	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
44	43	3ad2ant2 1131	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
45		ssun4 4102	. . . . . . . . . . . 12 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
46	45, 3	sseqtrrdi 3966	. . . . . . . . . . 11 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
47	44, 46	syl 17	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
48	42, 47	sstrd 3925	. . . . . . . . 9 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
49	31, 48	bnj593 32126	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
50		nfcv 2955	. . . . . . . . . 10 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅)
51	50, 25	nfss 3907	. . . . . . . . 9 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵
52	51	nf5ri 2193	. . . . . . . 8 ⊢ ( pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵 → ∀𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
53	49, 52	bnj1397 32216	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
54		simpr 488	. . . . . . . 8 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
55	3	bnj1138 32170	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↔ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
56	54, 55	sylib 221	. . . . . . 7 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
57	17, 53, 56	mpjaodan 956	. . . . . 6 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
58	57	ralrimiva 3149	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
59		df-bnj19 32077	. . . . 5 ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
60	58, 59	sylibr 237	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅))
61	3	bnj931 32152	. . . . 5 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵
62	61	a1i 11	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
63		bnj1408.4	. . . 4 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
64	4, 60, 62, 63	syl3anbrc 1340	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜏)
65	1, 63	bnj1124 32370	. . 3 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
66	2, 64, 65	syl2anc 587	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
67		bnj906 32312	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
68		iunss1 4895	. . . . 5 ⊢ ( pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
69		unss2 4108	. . . . 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 3960	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
73		biid 264	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
74		biid 264	. . . 4 ⊢ ((𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶) ↔ (𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶))
75	71, 73, 74	bnj1136 32379	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐶)
76	72, 75	sseqtrrd 3956	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ trCl(𝑋, 𝐴, 𝑅))
77	66, 76	eqssd 3932	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∀wral 3106 Vcvv 3441 ∪ cun 3879 ⊆ wss 3881 ∪ ciun 4881 predc-bnj14 32068 FrSe w-bnj15 32072 trClc-bnj18 32074 TrFow-bnj19 32076

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-reg 9040 ax-inf2 9088

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-om 7561 df-1o 8085 df-bnj17 32067 df-bnj14 32069 df-bnj13 32071 df-bnj15 32073 df-bnj18 32075 df-bnj19 32077

This theorem is referenced by: bnj1414 32419

W3C validator