bnj1398

Description: Technical lemma for bnj60 . 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.)

	Ref	Expression
Hypotheses	bnj1398.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
	bnj1398.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
	bnj1398.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
	bnj1398.4	⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
	bnj1398.5	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
	bnj1398.6	⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
	bnj1398.7	⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
	bnj1398.8	⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
	bnj1398.9	⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
	bnj1398.10	⊢ 𝑃 = ∪ 𝐻
	bnj1398.11	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
	bnj1398.12	⊢ ( 𝜂 ↔ ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
Assertion	bnj1398	⊢ ( 𝜒 → ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = dom 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		bnj1398.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj1398.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj1398.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj1398.4	⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5		bnj1398.5	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6		bnj1398.6	⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
7		bnj1398.7	⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8		bnj1398.8	⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
9		bnj1398.9	⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10		bnj1398.10	⊢ 𝑃 = ∪ 𝐻
11		bnj1398.11	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12		bnj1398.12	⊢ ( 𝜂 ↔ ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
13		df-iun	⊢ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) }
14	13	bnj1436	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
15	11 14	simplbiim	⊢ ( 𝜃 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
16		nfv	⊢ Ⅎ 𝑦 𝜓
17		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐷
18		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥
19	16 17 18	nf3an	⊢ Ⅎ 𝑦 ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 )
20	7 19	nfxfr	⊢ Ⅎ 𝑦 𝜒
21		nfiu1	⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
22	21	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
23	20 22	nfan	⊢ Ⅎ 𝑦 ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
24	11 23	nfxfr	⊢ Ⅎ 𝑦 𝜃
25	24	nf5ri	⊢ ( 𝜃 → ∀ 𝑦 𝜃 )
26	15 12 25	bnj1521	⊢ ( 𝜃 → ∃ 𝑦 𝜂 )
27		nfv	⊢ Ⅎ 𝑓 𝑅 FrSe 𝐴
28		nfe1	⊢ Ⅎ 𝑓 ∃ 𝑓 𝜏
29	28	nfn	⊢ Ⅎ 𝑓 ¬ ∃ 𝑓 𝜏
30		nfcv	⊢ Ⅎ 𝑓 𝐴
31	29 30	nfrabw	⊢ Ⅎ 𝑓 { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
32	5 31	nfcxfr	⊢ Ⅎ 𝑓 𝐷
33		nfcv	⊢ Ⅎ 𝑓 ∅
34	32 33	nfne	⊢ Ⅎ 𝑓 𝐷 ≠ ∅
35	27 34	nfan	⊢ Ⅎ 𝑓 ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ )
36	6 35	nfxfr	⊢ Ⅎ 𝑓 𝜓
37	32	nfcri	⊢ Ⅎ 𝑓 𝑥 ∈ 𝐷
38		nfv	⊢ Ⅎ 𝑓 ¬ 𝑦 𝑅 𝑥
39	32 38	nfralw	⊢ Ⅎ 𝑓 ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥
40	36 37 39	nf3an	⊢ Ⅎ 𝑓 ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 )
41	7 40	nfxfr	⊢ Ⅎ 𝑓 𝜒
42		nfv	⊢ Ⅎ 𝑓 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
43	41 42	nfan	⊢ Ⅎ 𝑓 ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
44	11 43	nfxfr	⊢ Ⅎ 𝑓 𝜃
45		nfv	⊢ Ⅎ 𝑓 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 )
46		nfv	⊢ Ⅎ 𝑓 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
47	44 45 46	nf3an	⊢ Ⅎ 𝑓 ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
48	12 47	nfxfr	⊢ Ⅎ 𝑓 𝜂
49	48	nf5ri	⊢ ( 𝜂 → ∀ 𝑓 𝜂 )
50	11	simplbi	⊢ ( 𝜃 → 𝜒 )
51	12 50	bnj835	⊢ ( 𝜂 → 𝜒 )
52	12	simp2bi	⊢ ( 𝜂 → 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) )
53	1 2 3 4 5 6 7 8	bnj1388	⊢ ( 𝜒 → ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∃ 𝑓 𝜏′ )
54		rsp	⊢ ( ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∃ 𝑓 𝜏′ → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ∃ 𝑓 𝜏′ ) )
55	53 54	syl	⊢ ( 𝜒 → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ∃ 𝑓 𝜏′ ) )
56	51 52 55	sylc	⊢ ( 𝜂 → ∃ 𝑓 𝜏′ )
57	49 56	bnj596	⊢ ( 𝜂 → ∃ 𝑓 ( 𝜂 ∧ 𝜏′ ) )
58	1 2 3 4 8	bnj1373	⊢ ( 𝜏′ ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
59	58	simplbi	⊢ ( 𝜏′ → 𝑓 ∈ 𝐶 )
60	59	adantl	⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑓 ∈ 𝐶 )
61	58	simprbi	⊢ ( 𝜏′ → dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
62		rspe	⊢ ( ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
63	52 61 62	syl2an	⊢ ( ( 𝜂 ∧ 𝜏′ ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
64	9	eqabri	⊢ ( 𝑓 ∈ 𝐻 ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ )
65	58	rexbii	⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
66		r19.42v	⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑓 ∈ 𝐶 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
67	64 65 66	3bitri	⊢ ( 𝑓 ∈ 𝐻 ↔ ( 𝑓 ∈ 𝐶 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
68	60 63 67	sylanbrc	⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑓 ∈ 𝐻 )
69	12	simp3bi	⊢ ( 𝜂 → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
70	69	adantr	⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
71	61	adantl	⊢ ( ( 𝜂 ∧ 𝜏′ ) → dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
72	70 71	eleqtrrd	⊢ ( ( 𝜂 ∧ 𝜏′ ) → 𝑧 ∈ dom 𝑓 )
73	68 72	jca	⊢ ( ( 𝜂 ∧ 𝜏′ ) → ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
74	57 73	bnj593	⊢ ( 𝜂 → ∃ 𝑓 ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
75		df-rex	⊢ ( ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 ↔ ∃ 𝑓 ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
76	74 75	sylibr	⊢ ( 𝜂 → ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
77	10	dmeqi	⊢ dom 𝑃 = dom ∪ 𝐻
78	9	bnj1317	⊢ ( 𝑤 ∈ 𝐻 → ∀ 𝑓 𝑤 ∈ 𝐻 )
79	78	bnj1400	⊢ dom ∪ 𝐻 = ∪ 𝑓 ∈ 𝐻 dom 𝑓
80	77 79	eqtri	⊢ dom 𝑃 = ∪ 𝑓 ∈ 𝐻 dom 𝑓
81	80	eleq2i	⊢ ( 𝑧 ∈ dom 𝑃 ↔ 𝑧 ∈ ∪ 𝑓 ∈ 𝐻 dom 𝑓 )
82		eliun	⊢ ( 𝑧 ∈ ∪ 𝑓 ∈ 𝐻 dom 𝑓 ↔ ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
83	81 82	bitri	⊢ ( 𝑧 ∈ dom 𝑃 ↔ ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
84	76 83	sylibr	⊢ ( 𝜂 → 𝑧 ∈ dom 𝑃 )
85	26 84	bnj593	⊢ ( 𝜃 → ∃ 𝑦 𝑧 ∈ dom 𝑃 )
86		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′
87	86	nfab	⊢ Ⅎ 𝑦 { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
88	9 87	nfcxfr	⊢ Ⅎ 𝑦 𝐻
89	88	nfuni	⊢ Ⅎ 𝑦 ∪ 𝐻
90	10 89	nfcxfr	⊢ Ⅎ 𝑦 𝑃
91	90	nfdm	⊢ Ⅎ 𝑦 dom 𝑃
92	91	nfcrii	⊢ ( 𝑧 ∈ dom 𝑃 → ∀ 𝑦 𝑧 ∈ dom 𝑃 )
93	85 92	bnj1397	⊢ ( 𝜃 → 𝑧 ∈ dom 𝑃 )
94	11 93	sylbir	⊢ ( ( 𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → 𝑧 ∈ dom 𝑃 )
95	94	ex	⊢ ( 𝜒 → ( 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ dom 𝑃 ) )
96	95	ssrdv	⊢ ( 𝜒 → ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ dom 𝑃 )
97		simpr	⊢ ( ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) → 𝑧 ∈ dom 𝑓 )
98	67	simprbi	⊢ ( 𝑓 ∈ 𝐻 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
99	98	adantr	⊢ ( ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
100		r19.42v	⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑧 ∈ dom 𝑓 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
101		eleq2	⊢ ( dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑧 ∈ dom 𝑓 ↔ 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
102	101	biimpac	⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
103	102	reximi	⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑧 ∈ dom 𝑓 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
104	100 103	sylbir	⊢ ( ( 𝑧 ∈ dom 𝑓 ∧ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
105	97 99 104	syl2anc	⊢ ( ( 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
106	105	rexlimiva	⊢ ( ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
107		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑧 ∈ ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
108	106 83 107	3imtr4i	⊢ ( 𝑧 ∈ dom 𝑃 → 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
109	108	ssriv	⊢ dom 𝑃 ⊆ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
110	109	a1i	⊢ ( 𝜒 → dom 𝑃 ⊆ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
111	96 110	eqssd	⊢ ( 𝜒 → ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) = dom 𝑃 )

Metamath Proof Explorer

Theorem bnj1398

Proof