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 31104

Description: Technical lemma for bnj1414 31105. 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 218	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜃)
3		bnj1408.1	. . . . 5 ⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
4	3	bnj1413 31103	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
5		simplll 798	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
6		bnj213 30952	. . . . . . . . . . 11 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
7	6	sseli 3599	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → 𝑧 ∈ 𝐴)
8	7	adantl 482	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
9		bnj906 31000	. . . . . . . . 9 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
10	5, 8, 9	syl2anc 693	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
11		bnj1318 31093	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → trCl(𝑦, 𝐴, 𝑅) = trCl(𝑧, 𝐴, 𝑅))
12	11	ssiun2s 4564	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
13		ssun4 3779	. . . . . . . . . . 11 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
14	13, 3	syl6sseqr 3652	. . . . . . . . . 10 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
15	12, 14	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
16	15	adantl 482	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
17	10, 16	sstrd 3613	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
18		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
19	18	bnj1405 30907	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 ∈ pred (𝑋, 𝐴, 𝑅)𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
20		biid 251	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) ↔ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
21		nfv 1843	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)
22		nfcv 2764	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 pred(𝑋, 𝐴, 𝑅)
23		nfiu1 4550	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
24	22, 23	nfun 3769	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
25	3, 24	nfcxfr 2762	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
26	25	nfcri 2758	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
27	21, 26	nfan 1828	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵)
28	23	nfcri 2758	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
29	27, 28	nfan 1828	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
30	29	nf5ri 2065	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∀𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
31	19, 20, 30	bnj1521 30921	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
32		simplll 798	. . . . . . . . . . . . 13 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
33	32	3ad2ant1 1082	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
34		bnj1147 31062	. . . . . . . . . . . . 13 ⊢ trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
35		simp3 1063	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
36	34, 35	bnj1213 30869	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
37	33, 36, 9	syl2anc 693	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
38		simp2 1062	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ pred(𝑋, 𝐴, 𝑅))
39	6, 38	bnj1213 30869	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴)
40		bnj1125 31060	. . . . . . . . . . . 12 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
41	33, 39, 35, 40	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
42	37, 41	sstrd 3613	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
43		ssiun2 4563	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
44	43	3ad2ant2 1083	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
45		ssun4 3779	. . . . . . . . . . . 12 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
46	45, 3	syl6sseqr 3652	. . . . . . . . . . 11 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
47	44, 46	syl 17	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
48	42, 47	sstrd 3613	. . . . . . . . 9 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
49	31, 48	bnj593 30815	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
50		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅)
51	50, 25	nfss 3596	. . . . . . . . 9 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵
52	51	nf5ri 2065	. . . . . . . 8 ⊢ ( pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵 → ∀𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
53	49, 52	bnj1397 30905	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
54		simpr 477	. . . . . . . 8 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
55	3	bnj1138 30859	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↔ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
56	54, 55	sylib 208	. . . . . . 7 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
57	17, 53, 56	mpjaodan 827	. . . . . 6 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
58	57	ralrimiva 2966	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
59		df-bnj19 30763	. . . . 5 ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
60	58, 59	sylibr 224	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅))
61	3	bnj931 30841	. . . . 5 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵
62	61	a1i 11	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
63		bnj1408.4	. . . 4 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
64	4, 60, 62, 63	syl3anbrc 1246	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜏)
65	1, 63	bnj1124 31056	. . 3 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
66	2, 64, 65	syl2anc 693	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
67		bnj906 31000	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
68		iunss1 4532	. . . . 5 ⊢ ( pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
69		unss2 3784	. . . . 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 3646	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
73		biid 251	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
74		biid 251	. . . 4 ⊢ ((𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶) ↔ (𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶))
75	71, 73, 74	bnj1136 31065	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐶)
76	72, 75	sseqtr4d 3642	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ trCl(𝑋, 𝐴, 𝑅))
77	66, 76	eqssd 3620	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 ∪ cun 3572 ⊆ wss 3574 ∪ ciun 4520 predc-bnj14 30754 FrSe w-bnj15 30758 trClc-bnj18 30760 TrFow-bnj19 30762

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-reg 8497 ax-inf2 8538

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-om 7066 df-1o 7560 df-bnj17 30753 df-bnj14 30755 df-bnj13 30757 df-bnj15 30759 df-bnj18 30761 df-bnj19 30763

This theorem is referenced by: bnj1414 31105

W3C validator